src/HOL/Inductive.thy
changeset 15131 c69542757a4d
parent 14981 e73f8140af78
child 15140 322485b816ac
equal deleted inserted replaced
15130:dc6be28d7f4e 15131:c69542757a4d
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
     4 *)
     4 *)
     5 
     5 
     6 header {* Support for inductive sets and types *}
     6 header {* Support for inductive sets and types *}
     7 
     7 
     8 theory Inductive = Gfp + Sum_Type + Relation + Record
     8 theory Inductive 
       
     9 import Gfp Sum_Type Relation Record
     9 files
    10 files
    10   ("Tools/inductive_package.ML")
    11   ("Tools/inductive_package.ML")
    11   ("Tools/inductive_realizer.ML")
    12   ("Tools/inductive_realizer.ML")
    12   ("Tools/inductive_codegen.ML")
    13   ("Tools/inductive_codegen.ML")
    13   ("Tools/datatype_aux.ML")
    14   ("Tools/datatype_aux.ML")
    16   ("Tools/datatype_abs_proofs.ML")
    17   ("Tools/datatype_abs_proofs.ML")
    17   ("Tools/datatype_realizer.ML")
    18   ("Tools/datatype_realizer.ML")
    18   ("Tools/datatype_package.ML")
    19   ("Tools/datatype_package.ML")
    19   ("Tools/datatype_codegen.ML")
    20   ("Tools/datatype_codegen.ML")
    20   ("Tools/recfun_codegen.ML")
    21   ("Tools/recfun_codegen.ML")
    21   ("Tools/primrec_package.ML"):
    22   ("Tools/primrec_package.ML")
    22 
    23 begin
    23 
    24 
    24 subsection {* Inductive sets *}
    25 subsection {* Inductive sets *}
    25 
    26 
    26 text {* Inversion of injective functions. *}
    27 text {* Inversion of injective functions. *}
    27 
    28