src/HOLCF/Tutorial/New_Domain.thy
changeset 39974 b525988432e9
parent 37000 41a22e7c1145
child 39986 38677db30cad
     1.1 --- a/src/HOLCF/Tutorial/New_Domain.thy	Tue Oct 05 17:53:00 2010 -0700
     1.2 +++ b/src/HOLCF/Tutorial/New_Domain.thy	Wed Oct 06 10:49:27 2010 -0700
     1.3 @@ -9,14 +9,14 @@
     1.4  begin
     1.5  
     1.6  text {*
     1.7 -  The definitional domain package only works with representable domains,
     1.8 -  i.e. types in class @{text rep}.
     1.9 +  The definitional domain package only works with SFP domains,
    1.10 +  i.e. types in class @{text sfp}.
    1.11  *}
    1.12  
    1.13 -default_sort rep
    1.14 +default_sort sfp
    1.15  
    1.16  text {*
    1.17 -  Provided that @{text rep} is the default sort, the @{text new_domain}
    1.18 +  Provided that @{text sfp} is the default sort, the @{text new_domain}
    1.19    package should work with any type definition supported by the old
    1.20    domain package.
    1.21  *}