changeset 57488 | 8453d35e4684 |
parent 57411 | 451d5b73f8cf |
child 57617 | 600f432ab556 |
1.1 --- a/etc/isar-keywords-ZF.el Fri Mar 14 15:26:52 2014 +0100 1.2 +++ b/etc/isar-keywords-ZF.el Fri Mar 14 15:41:29 2014 +0100 1.3 @@ -367,6 +367,7 @@ 1.4 "hide_fact" 1.5 "hide_type" 1.6 "inductive" 1.7 + "inductive_cases" 1.8 "instantiation" 1.9 "judgment" 1.10 "lemmas" 1.11 @@ -404,7 +405,7 @@ 1.12 "typedecl")) 1.13 1.14 (defconst isar-keywords-theory-script 1.15 - '("inductive_cases")) 1.16 + '()) 1.17 1.18 (defconst isar-keywords-theory-goal 1.19 '("corollary"