--- a/src/HOLCF/Tutorial/New_Domain.thy Tue Oct 05 17:53:00 2010 -0700
+++ b/src/HOLCF/Tutorial/New_Domain.thy Wed Oct 06 10:49:27 2010 -0700
@@ -9,14 +9,14 @@
begin
text {*
- The definitional domain package only works with representable domains,
- i.e. types in class @{text rep}.
+ The definitional domain package only works with SFP domains,
+ i.e. types in class @{text sfp}.
*}
-default_sort rep
+default_sort sfp
text {*
- Provided that @{text rep} is the default sort, the @{text new_domain}
+ Provided that @{text sfp} is the default sort, the @{text new_domain}
package should work with any type definition supported by the old
domain package.
*}