--- a/src/HOLCF/Fix.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Fix.thy Fri Oct 10 19:02:28 1997 +0200
@@ -20,14 +20,14 @@
defs
-iterate_def "iterate n F c == nat_rec c (%n x.F`x) n"
-Ifix_def "Ifix F == lub(range(%i.iterate i F UU))"
+iterate_def "iterate n F c == nat_rec c (%n x. F`x) n"
+Ifix_def "Ifix F == lub(range(%i. iterate i F UU))"
fix_def "fix == (LAM f. Ifix f)"
adm_def "adm P == !Y. is_chain(Y) -->
- (!i.P(Y i)) --> P(lub(range Y))"
+ (!i. P(Y i)) --> P(lub(range Y))"
-admw_def "admw P == !F. (!n.P (iterate n F UU)) -->
+admw_def "admw P == !F. (!n. P (iterate n F UU)) -->
P (lub(range (%i. iterate i F UU)))"
end