src/HOL/Product_Type.thy
changeset 33959 2afc55e8ed27
parent 33638 548a34929e98
child 34886 873c31d9f10d
equal deleted inserted replaced
33958:a57f4c9d0a19 33959:2afc55e8ed27
     4 *)
     4 *)
     5 
     5 
     6 header {* Cartesian products *}
     6 header {* Cartesian products *}
     7 
     7 
     8 theory Product_Type
     8 theory Product_Type
     9 imports Inductive
     9 imports Typedef Inductive Fun
    10 uses
    10 uses
    11   ("Tools/split_rule.ML")
    11   ("Tools/split_rule.ML")
    12   ("Tools/inductive_set.ML")
    12   ("Tools/inductive_set.ML")
    13   ("Tools/inductive_realizer.ML")
       
    14   ("Tools/Datatype/datatype_realizer.ML")
       
    15 begin
    13 begin
    16 
    14 
    17 subsection {* @{typ bool} is a datatype *}
    15 subsection {* @{typ bool} is a datatype *}
    18 
    16 
    19 rep_datatype True False by (auto intro: bool_induct)
    17 rep_datatype True False by (auto intro: bool_induct)
  1193 val unit_all_eq1 = thm "unit_all_eq1";
  1191 val unit_all_eq1 = thm "unit_all_eq1";
  1194 val unit_all_eq2 = thm "unit_all_eq2";
  1192 val unit_all_eq2 = thm "unit_all_eq2";
  1195 val unit_eq = thm "unit_eq";
  1193 val unit_eq = thm "unit_eq";
  1196 *}
  1194 *}
  1197 
  1195 
  1198 
       
  1199 subsection {* Further inductive packages *}
       
  1200 
       
  1201 use "Tools/inductive_realizer.ML"
       
  1202 setup InductiveRealizer.setup
       
  1203 
       
  1204 use "Tools/inductive_set.ML"
  1196 use "Tools/inductive_set.ML"
  1205 setup Inductive_Set.setup
  1197 setup Inductive_Set.setup
  1206 
  1198 
  1207 use "Tools/Datatype/datatype_realizer.ML"
       
  1208 setup DatatypeRealizer.setup
       
  1209 
       
  1210 end
  1199 end