src/ZF/Inductive_ZF.thy
changeset 46947 b8c7eb0c2f89
parent 46821 ff6b0c1087f2
child 46950 d0181abdbdac
     1.1 --- a/src/ZF/Inductive_ZF.thy	Thu Mar 15 17:45:54 2012 +0100
     1.2 +++ b/src/ZF/Inductive_ZF.thy	Thu Mar 15 19:02:34 2012 +0100
     1.3 @@ -13,6 +13,9 @@
     1.4  
     1.5  theory Inductive_ZF
     1.6  imports Fixedpt QPair Nat_ZF
     1.7 +keywords
     1.8 +  "elimination" "induction" "case_eqns" "recursor_eqns"
     1.9 +  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
    1.10  uses
    1.11    ("ind_syntax.ML")
    1.12    ("Tools/cartprod.ML")