# HG changeset patch
# User wenzelm
# Date 1191681682 -7200
# Node ID 6e6d9e80ebb46df569ec960c907b16a8877b0f31
# Parent  62c48c4bee4873e1423d78f6a5a74fa12e6b5a81
updated;

diff -r 62c48c4bee48 -r 6e6d9e80ebb4 etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Fri Oct 05 23:04:17 2007 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el	Sat Oct 06 16:41:22 2007 +0200
@@ -42,6 +42,7 @@
     "code_const"
     "code_datatype"
     "code_deps"
+    "code_exception"
     "code_instance"
     "code_library"
     "code_module"
@@ -263,6 +264,7 @@
     "inject"
     "invariant"
     "is"
+    "local_syntax"
     "module_name"
     "monos"
     "morphisms"
@@ -392,6 +394,7 @@
     "code_class"
     "code_const"
     "code_datatype"
+    "code_exception"
     "code_instance"
     "code_library"
     "code_module"
diff -r 62c48c4bee48 -r 6e6d9e80ebb4 etc/isar-keywords-ZF.el
--- 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"))
diff -r 62c48c4bee48 -r 6e6d9e80ebb4 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Oct 05 23:04:17 2007 +0200
+++ b/etc/isar-keywords.el	Sat Oct 06 16:41:22 2007 +0200
@@ -42,6 +42,7 @@
     "code_const"
     "code_datatype"
     "code_deps"
+    "code_exception"
     "code_instance"
     "code_library"
     "code_module"
@@ -268,6 +269,7 @@
     "internals"
     "is"
     "lazy"
+    "local_syntax"
     "module_name"
     "monos"
     "morphisms"
@@ -407,6 +409,7 @@
     "code_class"
     "code_const"
     "code_datatype"
+    "code_exception"
     "code_instance"
     "code_library"
     "code_module"