src/ZF/Inductive_ZF.thy

--- a/src/ZF/Inductive_ZF.thy	Thu Mar 15 17:45:54 2012 +0100
+++ b/src/ZF/Inductive_ZF.thy	Thu Mar 15 19:02:34 2012 +0100
@@ -13,6 +13,9 @@
 
 theory Inductive_ZF
 imports Fixedpt QPair Nat_ZF
+keywords
+  "elimination" "induction" "case_eqns" "recursor_eqns"
+  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
 uses
   ("ind_syntax.ML")
   ("Tools/cartprod.ML")