--- a/src/HOLCF/One.thy Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/One.thy Thu Jun 29 16:28:40 1995 +0200
@@ -29,12 +29,12 @@
one_when :: "'c -> one -> 'c"
rules
- abs_one_iso "abs_one[rep_one[u]] = u"
- rep_one_iso "rep_one[abs_one[x]] = x"
+ abs_one_iso "abs_one`(rep_one`u) = u"
+ rep_one_iso "rep_one`(abs_one`x) = x"
- one_def "one == abs_one[up[UU]]"
- one_when_def "one_when == (LAM c u.lift[LAM x.c][rep_one[u]])"
-
+defs
+ one_def "one == abs_one`(up`UU)"
+ one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
end