src/HOLCF/Tutorial/New_Domain.thy
changeset 39986 38677db30cad
parent 39974 b525988432e9
child 40329 73f2b99b549d
     1.1 --- a/src/HOLCF/Tutorial/New_Domain.thy	Thu Oct 07 13:54:43 2010 -0700
     1.2 +++ b/src/HOLCF/Tutorial/New_Domain.thy	Fri Oct 08 07:39:50 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 SFP domains,
     1.8 -  i.e. types in class @{text sfp}.
     1.9 +  The definitional domain package only works with bifinite domains,
    1.10 +  i.e. types in class @{text bifinite}.
    1.11  *}
    1.12  
    1.13 -default_sort sfp
    1.14 +default_sort bifinite
    1.15  
    1.16  text {*
    1.17 -  Provided that @{text sfp} is the default sort, the @{text new_domain}
    1.18 +  Provided that @{text bifinite} 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  *}