eliminated rules;
tuned;

--- a/src/HOLCF/One.thy	Thu Sep 25 13:25:50 1997 +0200
+++ b/src/HOLCF/One.thy	Fri Sep 26 10:12:04 1997 +0200
@@ -6,16 +6,13 @@
 
 One = Lift +
 
-types one = "unit lift"
+types one = unit lift
 
-consts
-	ONE             :: "one"
+constdefs
+  ONE :: "one"
+  "ONE == Def ()"
 
 translations
-	     "one" == (type) "unit lift" 
+  "one" <= (type) "unit lift" 
 
-rules
-  ONE_def     "ONE == Def()"
 end
-
-