diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2005-09-22 18:51:32 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2005-09-22 18:51:32 +0000 |
| commit | da1430884d485384b3e106d4add309feb4147cac (patch) | |
| tree | 31fa0dfd78c9e5cc743110e0fbbe8a65960a83f7 /isar/isar-keywords.el | |
| parent | 00efc2cea2d1c0acbaec3612c7974cd37988a953 (diff) | |
updated from pre-Isabelle2005;
Diffstat (limited to 'isar/isar-keywords.el')
| -rw-r--r-- | isar/isar-keywords.el | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el index da1f5f0e..d42c682e 100644 --- a/isar/isar-keywords.el +++ b/isar/isar-keywords.el @@ -44,6 +44,8 @@ "classes" "classrel" "clear_undos" + "code_library" + "code_module" "coinductive" "commit" "constdefs" @@ -70,12 +72,12 @@ "extract_type" "finalconsts" "finally" + "find_theorems" "fix" "fixpat" "fixrec" "from" "full_prf" - "generate_code" "global" "have" "header" @@ -172,7 +174,6 @@ "theory" "thm" "thm_deps" - "thms_containing" "thus" "token_translation" "touch_all_thys" @@ -196,6 +197,7 @@ "use_thy" "use_thy_only" "using" + "value" "welcome" "with" "{" @@ -213,8 +215,10 @@ "concl" "congs" "constrains" + "contains" "defines" "distinct" + "file" "files" "fixes" "hide_action" @@ -284,6 +288,7 @@ "disable_pr" "display_drafts" "enable_pr" + "find_theorems" "full_prf" "header" "kill_thy" @@ -318,7 +323,6 @@ "term" "thm" "thm_deps" - "thms_containing" "touch_all_thys" "touch_child_thys" "touch_thy" @@ -328,6 +332,7 @@ "use" "use_thy" "use_thy_only" + "value" "welcome")) (defconst isar-keywords-theory-begin @@ -353,6 +358,8 @@ "axioms" "classes" "classrel" + "code_library" + "code_module" "coinductive" "constdefs" "consts" @@ -367,7 +374,6 @@ "finalconsts" "fixpat" "fixrec" - "generate_code" "global" "hide" "inductive" |