src/HOLCF/Tutorial/New_Domain.thy
changeset 40329 73f2b99b549d
parent 39986 38677db30cad
child 40497 d2e876d6da8c
     1.1 --- a/src/HOLCF/Tutorial/New_Domain.thy	Sat Oct 30 12:25:18 2010 -0700
     1.2 +++ b/src/HOLCF/Tutorial/New_Domain.thy	Sat Oct 30 15:13:11 2010 -0700
     1.3 @@ -9,8 +9,8 @@
     1.4  begin
     1.5  
     1.6  text {*
     1.7 -  The definitional domain package only works with bifinite domains,
     1.8 -  i.e. types in class @{text bifinite}.
     1.9 +  UPDATE: The definitional back-end is now the default mode of the domain
    1.10 +  package. This file should be merged with @{text Domain_ex.thy}.
    1.11  *}
    1.12  
    1.13  default_sort bifinite
    1.14 @@ -21,7 +21,7 @@
    1.15    domain package.
    1.16  *}
    1.17  
    1.18 -new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
    1.19 +domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
    1.20  
    1.21  text {*
    1.22    The difference is that the new domain package is completely
    1.23 @@ -38,7 +38,7 @@
    1.24    indirect recursion through the lazy list type constructor.
    1.25  *}
    1.26  
    1.27 -new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
    1.28 +domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
    1.29  
    1.30  text {*
    1.31    For indirect-recursive definitions, the domain package is not able to