--- a/etc/isar-keywords-ZF.el Fri Oct 05 23:04:17 2007 +0200
+++ b/etc/isar-keywords-ZF.el Sat Oct 06 16:41:22 2007 +0200
@@ -38,10 +38,13 @@
"classrel"
"codatatype"
"code_datatype"
+ "code_library"
+ "code_module"
"coinductive"
"commit"
"constdefs"
"consts"
+ "consts_code"
"context"
"corollary"
"datatype"
@@ -77,6 +80,8 @@
"inductive_cases"
"init_toplevel"
"instance"
+ "instance_proof"
+ "instantiation"
"interpret"
"interpretation"
"invoke"
@@ -139,6 +144,8 @@
"prop"
"pwd"
"qed"
+ "quickcheck"
+ "quickcheck_params"
"quit"
"realizability"
"realizers"
@@ -177,6 +184,7 @@
"typed_print_translation"
"typedecl"
"types"
+ "types_code"
"ultimately"
"undo"
"undos_proof"
@@ -184,6 +192,7 @@
"use"
"use_thy"
"using"
+ "value"
"welcome"
"with"
"{"
@@ -200,9 +209,11 @@
"con_defs"
"concl"
"constrains"
+ "contains"
"defines"
"domains"
"elimination"
+ "file"
"fixes"
"for"
"identifier"
@@ -216,6 +227,7 @@
"infixr"
"intros"
"is"
+ "local_syntax"
"monos"
"notes"
"obtains"
@@ -292,6 +304,7 @@
"print_trans_rules"
"prop"
"pwd"
+ "quickcheck"
"remove_thy"
"term"
"thm"
@@ -302,6 +315,7 @@
"typ"
"use"
"use_thy"
+ "value"
"welcome"))
(defconst isar-keywords-theory-begin
@@ -331,9 +345,12 @@
"classrel"
"codatatype"
"code_datatype"
+ "code_library"
+ "code_module"
"coinductive"
"constdefs"
"consts"
+ "consts_code"
"context"
"datatype"
"declaration"
@@ -347,6 +364,7 @@
"global"
"hide"
"inductive"
+ "instantiation"
"judgment"
"lemmas"
"local"
@@ -362,6 +380,7 @@
"primrec"
"print_ast_translation"
"print_translation"
+ "quickcheck_params"
"realizability"
"realizers"
"rep_datatype"
@@ -375,7 +394,8 @@
"translations"
"typed_print_translation"
"typedecl"
- "types"))
+ "types"
+ "types_code"))
(defconst isar-keywords-theory-script
'("inductive_cases"))
@@ -383,6 +403,7 @@
(defconst isar-keywords-theory-goal
'("corollary"
"instance"
+ "instance_proof"
"interpretation"
"lemma"
"theorem"))