src/HOLCF/One.thy
changeset 3717 e28553315355
parent 2640 ee4dfce170a0
child 12030 46d57d0290a2
     1.1 --- a/src/HOLCF/One.thy	Thu Sep 25 13:25:50 1997 +0200
     1.2 +++ b/src/HOLCF/One.thy	Fri Sep 26 10:12:04 1997 +0200
     1.3 @@ -6,16 +6,13 @@
     1.4  
     1.5  One = Lift +
     1.6  
     1.7 -types one = "unit lift"
     1.8 +types one = unit lift
     1.9  
    1.10 -consts
    1.11 -	ONE             :: "one"
    1.12 +constdefs
    1.13 +  ONE :: "one"
    1.14 +  "ONE == Def ()"
    1.15  
    1.16  translations
    1.17 -	     "one" == (type) "unit lift" 
    1.18 +  "one" <= (type) "unit lift" 
    1.19  
    1.20 -rules
    1.21 -  ONE_def     "ONE == Def()"
    1.22  end
    1.23 -
    1.24 -