src/HOL/Datatype.thy
changeset 42163 392fd6c4669c
parent 41505 6d19301074cf
child 45607 16b4f5774621
     1.1 --- a/src/HOL/Datatype.thy	Wed Mar 30 11:32:51 2011 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Mar 30 11:32:52 2011 +0200
     1.3 @@ -28,8 +28,8 @@
     1.4  
     1.5  text{*Datatypes will be represented by sets of type @{text node}*}
     1.6  
     1.7 -types 'a item        = "('a, unit) node set"
     1.8 -      ('a, 'b) dtree = "('a, 'b) node set"
     1.9 +type_synonym 'a item        = "('a, unit) node set"
    1.10 +type_synonym ('a, 'b) dtree = "('a, 'b) node set"
    1.11  
    1.12  consts
    1.13    Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"