src/HOLCF/Tutorial/New_Domain.thy
changeset 40497 d2e876d6da8c
parent 40329 73f2b99b549d
     1.1 --- a/src/HOLCF/Tutorial/New_Domain.thy	Wed Nov 10 09:59:08 2010 -0800
     1.2 +++ b/src/HOLCF/Tutorial/New_Domain.thy	Wed Nov 10 11:42:35 2010 -0800
     1.3 @@ -13,10 +13,8 @@
     1.4    package. This file should be merged with @{text Domain_ex.thy}.
     1.5  *}
     1.6  
     1.7 -default_sort bifinite
     1.8 -
     1.9  text {*
    1.10 -  Provided that @{text bifinite} is the default sort, the @{text new_domain}
    1.11 +  Provided that @{text domain} is the default sort, the @{text new_domain}
    1.12    package should work with any type definition supported by the old
    1.13    domain package.
    1.14  *}