etc/isar-keywords-ZF.el
changeset 56146 8453d35e4684
parent 56069 451d5b73f8cf
child 56275 600f432ab556
--- a/etc/isar-keywords-ZF.el	Fri Mar 14 15:26:52 2014 +0100
+++ b/etc/isar-keywords-ZF.el	Fri Mar 14 15:41:29 2014 +0100
@@ -367,6 +367,7 @@
     "hide_fact"
     "hide_type"
     "inductive"
+    "inductive_cases"
     "instantiation"
     "judgment"
     "lemmas"
@@ -404,7 +405,7 @@
     "typedecl"))
 
 (defconst isar-keywords-theory-script
-  '("inductive_cases"))
+  '())
 
 (defconst isar-keywords-theory-goal
   '("corollary"