src/HOLCF/One.thy
changeset 1168 74be52691d62
parent 625 119391dd1d59
child 1274 ea0668a1c0ba
     1.1 --- a/src/HOLCF/One.thy	Thu Jun 29 16:16:24 1995 +0200
     1.2 +++ b/src/HOLCF/One.thy	Thu Jun 29 16:28:40 1995 +0200
     1.3 @@ -29,12 +29,12 @@
     1.4  	one_when 	:: "'c -> one -> 'c"
     1.5  
     1.6  rules
     1.7 -  abs_one_iso	"abs_one[rep_one[u]] = u"
     1.8 -  rep_one_iso  "rep_one[abs_one[x]] = x"
     1.9 +  abs_one_iso	"abs_one`(rep_one`u) = u"
    1.10 +  rep_one_iso	"rep_one`(abs_one`x) = x"
    1.11  
    1.12 -  one_def	"one == abs_one[up[UU]]"
    1.13 -  one_when_def "one_when == (LAM c u.lift[LAM x.c][rep_one[u]])"
    1.14 -
    1.15 +defs
    1.16 +  one_def	"one == abs_one`(up`UU)"
    1.17 +  one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
    1.18  end
    1.19  
    1.20