--- a/src/ZF/Inductive_ZF.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/ZF/Inductive_ZF.thy Thu Mar 15 22:08:53 2012 +0100
@@ -14,8 +14,10 @@
theory Inductive_ZF
imports Fixedpt QPair Nat_ZF
keywords
+ "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
+ "inductive_cases" :: thy_script and
+ "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
"elimination" "induction" "case_eqns" "recursor_eqns"
- "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
uses
("ind_syntax.ML")
("Tools/cartprod.ML")