# HG changeset patch
# User wenzelm
# Date 875261524 -7200
# Node ID e285533153553a7a2bd0520d34764ffae6879e92
# Parent  2885b760a4b41c3542a31da9e6e7452d138b468a
eliminated rules;
tuned;

diff -r 2885b760a4b4 -r e28553315355 src/HOLCF/One.thy
--- 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
-
-