# HG changeset patch
# User berghofe
# Date 1160757230 -7200
# Node ID 3f89f99d746e2cbcc4c801cccaf687f08a93a74b
# Parent  3b2821e0d541984fcec9e14dc7b0950219871df1
Added keywords for new inductive definition package.

diff -r 3b2821e0d541 -r 3f89f99d746e etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Oct 13 18:29:31 2006 +0200
+++ b/etc/isar-keywords.el	Fri Oct 13 18:33:50 2006 +0200
@@ -56,6 +56,7 @@
     "code_type"
     "code_typename"
     "coinductive"
+    "coinductive2"
     "commit"
     "const_syntax"
     "constdefs"
@@ -98,7 +99,9 @@
     "hence"
     "hide"
     "inductive"
+    "inductive2"
     "inductive_cases"
+    "inductive_cases2"
     "init_toplevel"
     "instance"
     "interpret"
@@ -211,7 +214,6 @@
     "types_code"
     "ultimately"
     "undo"
-    "undo_end"
     "undos_proof"
     "unfolding"
     "update_thy"
@@ -306,7 +308,6 @@
     "quit"
     "redo"
     "undo"
-    "undo_end"
     "undos_proof"))
 
 (defconst isar-keywords-diag
@@ -409,6 +410,7 @@
     "code_type"
     "code_typename"
     "coinductive"
+    "coinductive2"
     "const_syntax"
     "constdefs"
     "consts"
@@ -428,6 +430,7 @@
     "global"
     "hide"
     "inductive"
+    "inductive2"
     "judgment"
     "lemmas"
     "local"
@@ -463,7 +466,8 @@
 
 (defconst isar-keywords-theory-script
   '("declare"
-    "inductive_cases"))
+    "inductive_cases"
+    "inductive_cases2"))
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"