etc/isar-keywords-ZF.el

--- a/etc/isar-keywords-ZF.el	Mon May 11 09:18:42 2009 +0200
+++ b/etc/isar-keywords-ZF.el	Mon May 11 09:39:53 2009 +0200
@@ -45,15 +45,18 @@
     "class_deps"
     "classes"
     "classrel"
+    "codatatype"
     "code_datatype"
     "code_library"
     "code_module"
+    "coinductive"
     "commit"
     "constdefs"
     "consts"
     "consts_code"
     "context"
     "corollary"
+    "datatype"
     "declaration"
     "declare"
     "def"
@@ -83,6 +86,8 @@
     "help"
     "hence"
     "hide"
+    "inductive"
+    "inductive_cases"
     "init_toplevel"
     "instance"
     "instantiation"
@@ -118,6 +123,7 @@
     "presume"
     "pretty_setmargin"
     "prf"
+    "primrec"
     "print_abbrevs"
     "print_antiquotations"
     "print_ast_translation"
@@ -140,6 +146,7 @@
     "print_simpset"
     "print_statement"
     "print_syntax"
+    "print_tcset"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
@@ -154,6 +161,7 @@
     "realizability"
     "realizers"
     "remove_thy"
+    "rep_datatype"
     "sect"
     "section"
     "setup"
@@ -207,9 +215,13 @@
     "attach"
     "begin"
     "binder"
+    "case_eqns"
+    "con_defs"
     "constrains"
     "contains"
     "defines"
+    "domains"
+    "elimination"
     "file"
     "fixes"
     "for"
@@ -217,17 +229,23 @@
     "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"))
@@ -295,6 +313,7 @@
     "print_simpset"
     "print_statement"
     "print_syntax"
+    "print_tcset"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
@@ -338,13 +357,16 @@
     "class"
     "classes"
     "classrel"
+    "codatatype"
     "code_datatype"
     "code_library"
     "code_module"
+    "coinductive"
     "constdefs"
     "consts"
     "consts_code"
     "context"
+    "datatype"
     "declaration"
     "declare"
     "defaultsort"
@@ -355,6 +377,7 @@
     "finalconsts"
     "global"
     "hide"
+    "inductive"
     "instantiation"
     "judgment"
     "lemmas"
@@ -371,11 +394,13 @@
     "overloading"
     "parse_ast_translation"
     "parse_translation"
+    "primrec"
     "print_ast_translation"
     "print_translation"
     "quickcheck_params"
     "realizability"
     "realizers"
+    "rep_datatype"
     "setup"
     "simproc_setup"
     "syntax"
@@ -390,7 +415,7 @@
     "use"))
 
 (defconst isar-keywords-theory-script
-  '())
+  '("inductive_cases"))
 
 (defconst isar-keywords-theory-goal
   '("corollary"