src/HOL/Inductive.thy
changeset 13705 934d6c1421f2
parent 13469 70d8dfef587d
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Inductive.thy	Wed Nov 13 15:24:42 2002 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Wed Nov 13 15:25:17 2002 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4  theory Inductive = Gfp + Sum_Type + Relation + Record
     1.5  files
     1.6    ("Tools/inductive_package.ML")
     1.7 +  ("Tools/inductive_realizer.ML")
     1.8    ("Tools/inductive_codegen.ML")
     1.9    ("Tools/datatype_aux.ML")
    1.10    ("Tools/datatype_prop.ML")
    1.11 @@ -87,6 +88,9 @@
    1.12  use "Tools/datatype_codegen.ML"
    1.13  setup DatatypeCodegen.setup
    1.14  
    1.15 +use "Tools/inductive_realizer.ML"
    1.16 +setup InductiveRealizer.setup
    1.17 +
    1.18  use "Tools/inductive_codegen.ML"
    1.19  setup InductiveCodegen.setup
    1.20