src/HOL/Product_Type.thy
changeset 33959 2afc55e8ed27
parent 33638 548a34929e98
child 34886 873c31d9f10d
     1.1 --- a/src/HOL/Product_Type.thy	Wed Nov 25 09:14:28 2009 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Nov 25 11:16:57 2009 +0100
     1.3 @@ -6,12 +6,10 @@
     1.4  header {* Cartesian products *}
     1.5  
     1.6  theory Product_Type
     1.7 -imports Inductive
     1.8 +imports Typedef Inductive Fun
     1.9  uses
    1.10    ("Tools/split_rule.ML")
    1.11    ("Tools/inductive_set.ML")
    1.12 -  ("Tools/inductive_realizer.ML")
    1.13 -  ("Tools/Datatype/datatype_realizer.ML")
    1.14  begin
    1.15  
    1.16  subsection {* @{typ bool} is a datatype *}
    1.17 @@ -1195,16 +1193,7 @@
    1.18  val unit_eq = thm "unit_eq";
    1.19  *}
    1.20  
    1.21 -
    1.22 -subsection {* Further inductive packages *}
    1.23 -
    1.24 -use "Tools/inductive_realizer.ML"
    1.25 -setup InductiveRealizer.setup
    1.26 -
    1.27  use "Tools/inductive_set.ML"
    1.28  setup Inductive_Set.setup
    1.29  
    1.30 -use "Tools/Datatype/datatype_realizer.ML"
    1.31 -setup DatatypeRealizer.setup
    1.32 -
    1.33  end