src/HOL/Datatype.thy
changeset 45694 4a8743618257
parent 45607 16b4f5774621
child 46950 d0181abdbdac
     1.1 --- a/src/HOL/Datatype.thy	Wed Nov 30 16:05:15 2011 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Wed Nov 30 16:27:10 2011 +0100
     1.3 @@ -21,10 +21,11 @@
     1.4  
     1.5  subsection {* The datatype universe *}
     1.6  
     1.7 -typedef (Node)
     1.8 -  ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
     1.9 -    --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
    1.10 -  by auto
    1.11 +definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
    1.12 +
    1.13 +typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
    1.14 +  morphisms Rep_Node Abs_Node
    1.15 +  unfolding Node_def by auto
    1.16  
    1.17  text{*Datatypes will be represented by sets of type @{text node}*}
    1.18