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"