# HG changeset patch
# User wenzelm
# Date 1160771429 -7200
# Node ID ed94ba5139896e5dc9a28c9e393c1c65bd1632c8
# Parent  3f89f99d746e2cbcc4c801cccaf687f08a93a74b
updated;

diff -r 3f89f99d746e -r ed94ba513989 etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Fri Oct 13 18:33:50 2006 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el	Fri Oct 13 22:30:29 2006 +0200
@@ -53,9 +53,11 @@
     "code_instname"
     "code_library"
     "code_module"
+    "code_reserved"
     "code_type"
     "code_typename"
     "coinductive"
+    "coinductive2"
     "commit"
     "const_syntax"
     "constdefs"
@@ -94,7 +96,9 @@
     "hence"
     "hide"
     "inductive"
+    "inductive2"
     "inductive_cases"
+    "inductive_cases2"
     "init_toplevel"
     "instance"
     "interpret"
@@ -207,7 +211,6 @@
     "types_code"
     "ultimately"
     "undo"
-    "undo_end"
     "undos_proof"
     "unfolding"
     "update_thy"
@@ -285,7 +288,6 @@
     "quit"
     "redo"
     "undo"
-    "undo_end"
     "undos_proof"))
 
 (defconst isar-keywords-diag
@@ -385,9 +387,11 @@
     "code_instname"
     "code_library"
     "code_module"
+    "code_reserved"
     "code_type"
     "code_typename"
     "coinductive"
+    "coinductive2"
     "const_syntax"
     "constdefs"
     "consts"
@@ -404,6 +408,7 @@
     "global"
     "hide"
     "inductive"
+    "inductive2"
     "judgment"
     "lemmas"
     "local"
@@ -440,7 +445,8 @@
 
 (defconst isar-keywords-theory-script
   '("declare"
-    "inductive_cases"))
+    "inductive_cases"
+    "inductive_cases2"))
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
diff -r 3f89f99d746e -r ed94ba513989 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Fri Oct 13 18:33:50 2006 +0200
+++ b/etc/isar-keywords-ZF.el	Fri Oct 13 22:30:29 2006 +0200
@@ -51,6 +51,7 @@
     "code_instname"
     "code_library"
     "code_module"
+    "code_reserved"
     "code_type"
     "code_typename"
     "coinductive"
@@ -194,7 +195,6 @@
     "types_code"
     "ultimately"
     "undo"
-    "undo_end"
     "undos_proof"
     "unfolding"
     "update_thy"
@@ -271,7 +271,6 @@
     "quit"
     "redo"
     "undo"
-    "undo_end"
     "undos_proof"))
 
 (defconst isar-keywords-diag
@@ -370,6 +369,7 @@
     "code_instname"
     "code_library"
     "code_module"
+    "code_reserved"
     "code_type"
     "code_typename"
     "coinductive"
diff -r 3f89f99d746e -r ed94ba513989 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Oct 13 18:33:50 2006 +0200
+++ b/etc/isar-keywords.el	Fri Oct 13 22:30:29 2006 +0200
@@ -53,6 +53,7 @@
     "code_instname"
     "code_library"
     "code_module"
+    "code_reserved"
     "code_type"
     "code_typename"
     "coinductive"
@@ -407,6 +408,7 @@
     "code_instname"
     "code_library"
     "code_module"
+    "code_reserved"
     "code_type"
     "code_typename"
     "coinductive"