--- 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"
--- 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"
--- 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"