# HG changeset patch
# User berghofe
# Date 1184143940 -7200
# Node ID f9f89b7cfdc7586a50a0854db7c4ab66e5533fb6
# Parent  e42f71809a7a7871a2f2ec7b54cb7f302d31c720
Adapted to changes in inductive definition package.

diff -r e42f71809a7a -r f9f89b7cfdc7 etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Wed Jul 11 00:46:48 2007 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el	Wed Jul 11 10:52:20 2007 +0200
@@ -55,7 +55,7 @@
     "code_thms"
     "code_type"
     "coinductive"
-    "coinductive2"
+    "coinductive_set"
     "commit"
     "constdefs"
     "consts"
@@ -96,9 +96,8 @@
     "hence"
     "hide"
     "inductive"
-    "inductive2"
     "inductive_cases"
-    "inductive_cases2"
+    "inductive_set"
     "init_toplevel"
     "instance"
     "interpret"
@@ -261,7 +260,6 @@
     "infixl"
     "infixr"
     "inject"
-    "intros"
     "invariant"
     "is"
     "monos"
@@ -404,7 +402,7 @@
     "code_reserved"
     "code_type"
     "coinductive"
-    "coinductive2"
+    "coinductive_set"
     "constdefs"
     "consts"
     "consts_code"
@@ -423,7 +421,7 @@
     "global"
     "hide"
     "inductive"
-    "inductive2"
+    "inductive_set"
     "judgment"
     "lemmas"
     "local"
@@ -462,8 +460,7 @@
 
 (defconst isar-keywords-theory-script
   '("declare"
-    "inductive_cases"
-    "inductive_cases2"))
+    "inductive_cases"))
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
diff -r e42f71809a7a -r f9f89b7cfdc7 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Jul 11 00:46:48 2007 +0200
+++ b/etc/isar-keywords.el	Wed Jul 11 10:52:20 2007 +0200
@@ -55,7 +55,7 @@
     "code_thms"
     "code_type"
     "coinductive"
-    "coinductive2"
+    "coinductive_set"
     "commit"
     "constdefs"
     "consts"
@@ -99,9 +99,8 @@
     "hence"
     "hide"
     "inductive"
-    "inductive2"
     "inductive_cases"
-    "inductive_cases2"
+    "inductive_set"
     "init_toplevel"
     "instance"
     "interpret"
@@ -266,7 +265,6 @@
     "inject"
     "inputs"
     "internals"
-    "intros"
     "is"
     "lazy"
     "monos"
@@ -418,7 +416,7 @@
     "code_reserved"
     "code_type"
     "coinductive"
-    "coinductive2"
+    "coinductive_set"
     "constdefs"
     "consts"
     "consts_code"
@@ -439,7 +437,7 @@
     "global"
     "hide"
     "inductive"
-    "inductive2"
+    "inductive_set"
     "judgment"
     "lemmas"
     "local"
@@ -477,8 +475,7 @@
 
 (defconst isar-keywords-theory-script
   '("declare"
-    "inductive_cases"
-    "inductive_cases2"))
+    "inductive_cases"))
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"