--- a/src/HOLCF/Fix.thy Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/Fix.thy Thu Jun 29 16:28:40 1995 +0200
@@ -20,22 +20,22 @@
chain_finite :: "'a=>bool"
flat :: "'a=>bool"
-rules
+defs
-iterate_def "iterate(n,F,c) == nat_rec(n,c,%n x.F[x])"
-Ifix_def "Ifix(F) == lub(range(%i.iterate(i,F,UU)))"
-fix_def "fix == (LAM f. Ifix(f))"
+iterate_def "iterate n F c == nat_rec n c (%n x.F`x)"
+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)))"
+adm_def "adm P == !Y. is_chain(Y) -->
+ (!i.P(Y i)) --> P(lub(range Y))"
-admw_def "admw(P)== (!F.((!n.P(iterate(n,F,UU)))-->
- P(lub(range(%i.iterate(i,F,UU))))))"
+admw_def "admw P == !F. (!n.P (iterate n F UU)) -->
+ P (lub(range (%i. iterate i F UU)))"
-chain_finite_def "chain_finite(x::'a)==
- !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))"
+chain_finite_def "chain_finite (x::'a)==
+ !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)"
-flat_def "flat(x::'a) ==
+flat_def "flat (x::'a) ==
! x y. (x::'a) << y --> (x = UU) | (x=y)"
end