diff -r 5750eba8820d -r 66512c9e6bd6 src/HOLCF/Fix.thy
--- 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