src/HOL/Library/Old_Datatype.thy
changeset 58377 c6f93b8d2d8e
parent 58376 c9d3074f83b3
child 58390 b74d8470b98e
equal deleted inserted replaced
58376:c9d3074f83b3 58377:c6f93b8d2d8e
     7 
     7 
     8 theory Old_Datatype
     8 theory Old_Datatype
     9 imports "../Main"
     9 imports "../Main"
    10 keywords "old_datatype" :: thy_decl
    10 keywords "old_datatype" :: thy_decl
    11 begin
    11 begin
       
    12 
       
    13 ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
       
    14 ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
       
    15 
    12 
    16 
    13 subsection {* The datatype universe *}
    17 subsection {* The datatype universe *}
    14 
    18 
    15 definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
    19 definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
    16 
    20 
   521 hide_type (open) node item
   525 hide_type (open) node item
   522 hide_const (open) Push Node Atom Leaf Numb Lim Split Case
   526 hide_const (open) Push Node Atom Leaf Numb Lim Split Case
   523 
   527 
   524 ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
   528 ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
   525 ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
   529 ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
   526 ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
       
   527 
   530 
   528 end
   531 end