diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2001-08-31 16:44:22 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2001-08-31 16:44:22 +0000 |
| commit | da56e09479f29a48a0d8445c5e4f115e03fc2580 (patch) | |
| tree | eae1b16806a6a5fd4221e17e01f8879c9d304c2f /isar | |
| parent | 784c4ce5a05d54ab9da3902a46c7ad67bac5daa4 (diff) | |
new commands (proof terms, code generator);
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar-keywords.el | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el index d34c1830..07dc6c10 100644 --- a/isar/isar-keywords.el +++ b/isar/isar-keywords.el @@ -1,6 +1,6 @@ ;; ;; Keyword classification tables for Isabelle/Isar. -;; This file generated by Isabelle -- DO NOT EDIT! +;; This file was generated by Isabelle/HOLCF/IOA -- DO NOT EDIT! ;; ;; $Id$ ;; @@ -39,8 +39,8 @@ "commit" "constdefs" "consts" + "consts_code" "context" - "corollary" "datatype" "declare" "def" @@ -56,6 +56,8 @@ "finally" "fix" "from" + "full_prf" + "generate_code" "global" "have" "header" @@ -86,6 +88,7 @@ "prefer" "presume" "pretty_setmargin" + "prf" "primrec" "print_antiquotations" "print_ast_translation" @@ -147,6 +150,7 @@ "typedecl" "typedef" "types" + "types_code" "ultimately" "undo" "undos_proof" @@ -223,10 +227,12 @@ "commit" "disable_pr" "enable_pr" + "full_prf" "header" "kill_thy" "pr" "pretty_setmargin" + "prf" "print_antiquotations" "print_attributes" "print_binds" @@ -285,10 +291,12 @@ "coinductive" "constdefs" "consts" + "consts_code" "datatype" "defaultsort" "defer_recdef" "defs" + "generate_code" "global" "hide" "inductive" @@ -315,15 +323,15 @@ "translations" "typed_print_translation" "typedecl" - "types")) + "types" + "types_code")) (defconst isar-keywords-theory-script '("declare" "inductive_cases")) (defconst isar-keywords-theory-goal - '("corollary" - "instance" + '("instance" "lemma" "recdef_tc" "theorem" |