src/ZF/Inductive_ZF.thy
changeset 46950 d0181abdbdac
parent 46947 b8c7eb0c2f89
child 48891 c0eafbd55de3
     1.1 --- a/src/ZF/Inductive_ZF.thy	Thu Mar 15 20:07:00 2012 +0100
     1.2 +++ b/src/ZF/Inductive_ZF.thy	Thu Mar 15 22:08:53 2012 +0100
     1.3 @@ -14,8 +14,10 @@
     1.4  theory Inductive_ZF
     1.5  imports Fixedpt QPair Nat_ZF
     1.6  keywords
     1.7 +  "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
     1.8 +  "inductive_cases" :: thy_script and
     1.9 +  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
    1.10    "elimination" "induction" "case_eqns" "recursor_eqns"
    1.11 -  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
    1.12  uses
    1.13    ("ind_syntax.ML")
    1.14    ("Tools/cartprod.ML")