--- a/etc/isar-keywords-ZF.el Wed Apr 22 11:10:23 2009 +0200
+++ b/etc/isar-keywords-ZF.el Mon May 11 09:18:42 2009 +0200
@@ -18,7 +18,6 @@
"ML"
"ML_command"
"ML_prf"
- "ML_test"
"ML_val"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
@@ -46,18 +45,15 @@
"class_deps"
"classes"
"classrel"
- "codatatype"
"code_datatype"
"code_library"
"code_module"
- "coinductive"
"commit"
"constdefs"
"consts"
"consts_code"
"context"
"corollary"
- "datatype"
"declaration"
"declare"
"def"
@@ -87,8 +83,6 @@
"help"
"hence"
"hide"
- "inductive"
- "inductive_cases"
"init_toplevel"
"instance"
"instantiation"
@@ -124,7 +118,6 @@
"presume"
"pretty_setmargin"
"prf"
- "primrec"
"print_abbrevs"
"print_antiquotations"
"print_ast_translation"
@@ -147,7 +140,6 @@
"print_simpset"
"print_statement"
"print_syntax"
- "print_tcset"
"print_theorems"
"print_theory"
"print_trans_rules"
@@ -162,7 +154,6 @@
"realizability"
"realizers"
"remove_thy"
- "rep_datatype"
"sect"
"section"
"setup"
@@ -216,13 +207,9 @@
"attach"
"begin"
"binder"
- "case_eqns"
- "con_defs"
"constrains"
"contains"
"defines"
- "domains"
- "elimination"
"file"
"fixes"
"for"
@@ -230,23 +217,17 @@
"if"
"imports"
"in"
- "induction"
"infix"
"infixl"
"infixr"
- "intros"
"is"
- "monos"
"notes"
"obtains"
"open"
"output"
"overloaded"
- "recursor_eqns"
"shows"
"structure"
- "type_elims"
- "type_intros"
"unchecked"
"uses"
"where"))
@@ -314,7 +295,6 @@
"print_simpset"
"print_statement"
"print_syntax"
- "print_tcset"
"print_theorems"
"print_theory"
"print_trans_rules"
@@ -349,7 +329,6 @@
(defconst isar-keywords-theory-decl
'("ML"
- "ML_test"
"abbreviation"
"arities"
"attribute_setup"
@@ -359,16 +338,13 @@
"class"
"classes"
"classrel"
- "codatatype"
"code_datatype"
"code_library"
"code_module"
- "coinductive"
"constdefs"
"consts"
"consts_code"
"context"
- "datatype"
"declaration"
"declare"
"defaultsort"
@@ -379,7 +355,6 @@
"finalconsts"
"global"
"hide"
- "inductive"
"instantiation"
"judgment"
"lemmas"
@@ -396,13 +371,11 @@
"overloading"
"parse_ast_translation"
"parse_translation"
- "primrec"
"print_ast_translation"
"print_translation"
"quickcheck_params"
"realizability"
"realizers"
- "rep_datatype"
"setup"
"simproc_setup"
"syntax"
@@ -417,7 +390,7 @@
"use"))
(defconst isar-keywords-theory-script
- '("inductive_cases"))
+ '())
(defconst isar-keywords-theory-goal
'("corollary"