src/HOL/Inductive.thy
changeset 24625 0398a5e802d3
parent 24349 0dd8782fb02d
child 24626 85eceef2edc7
equal deleted inserted replaced
24624:b8383b1bbae3 24625:0398a5e802d3
     9 imports FixedPoint Product_Type Sum_Type
     9 imports FixedPoint Product_Type Sum_Type
    10 uses
    10 uses
    11   ("Tools/inductive_package.ML")
    11   ("Tools/inductive_package.ML")
    12   ("Tools/inductive_set_package.ML")
    12   ("Tools/inductive_set_package.ML")
    13   ("Tools/inductive_realizer.ML")
    13   ("Tools/inductive_realizer.ML")
       
    14   "Tools/dseq.ML"
    14   ("Tools/inductive_codegen.ML")
    15   ("Tools/inductive_codegen.ML")
    15   ("Tools/datatype_aux.ML")
    16   ("Tools/datatype_aux.ML")
    16   ("Tools/datatype_prop.ML")
    17   ("Tools/datatype_prop.ML")
    17   ("Tools/datatype_rep_proofs.ML")
    18   ("Tools/datatype_rep_proofs.ML")
    18   ("Tools/datatype_abs_proofs.ML")
    19   ("Tools/datatype_abs_proofs.ML")