--- a/src/HOLCF/Fix.thy Wed Jun 21 15:01:07 1995 +0200
+++ b/src/HOLCF/Fix.thy Wed Jun 21 15:14:58 1995 +0200
@@ -26,17 +26,17 @@
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) ==\
-\ ! x y. (x::'a) << y --> (x = UU) | (x=y)"
+flat_def "flat(x::'a) ==
+ ! x y. (x::'a) << y --> (x = UU) | (x=y)"
end