# HG changeset patch
# User clasohm
# Date 803833985 -7200
# Node ID 928a16e02f9f88817df2371c9556a6ff0a2953e8
# Parent  bc295e3dc078a814f98dfd23d054e024b81405c9
removed \...\ inside strings

diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/AC15_WO6.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -1,3 +1,3 @@
 (*Dummy theory to document dependencies *)
 
-AC15_WO6 = HH
\ No newline at end of file
+AC15_WO6 = HH
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/AC17_AC1.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -1,3 +1,3 @@
 (*Dummy theory to document dependencies *)
 
-AC17_AC1 = HH
\ No newline at end of file
+AC17_AC1 = HH
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/AC1_WO2.thy
--- a/src/ZF/AC/AC1_WO2.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/AC1_WO2.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -1,3 +1,3 @@
 (*Dummy theory to document dependencies *)
 
-AC1_WO2 = HH
\ No newline at end of file
+AC1_WO2 = HH
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -41,19 +41,19 @@
 
   WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
 
-  WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &   \
-\	             (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
+  WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &   
+	             (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
 
   WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
 
-  WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a   \
-\	            & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
+  WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a   
+	            & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
 
-  WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->   \
-\	            well_ord(A,converse(R)))"
+  WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->   
+	            well_ord(A,converse(R)))"
 
-  WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->  \
-\	            (EX R. well_ord(A,R))"
+  WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->  
+	            (EX R. well_ord(A,R))"
 
 (* Axioms of Choice *)  
 
@@ -61,65 +61,65 @@
 
   AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
 
-  AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)   \
-\	            --> (EX C. ALL B:A. EX y. B Int C = {y})"
+  AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)   
+	            --> (EX C. ALL B:A. EX y. B Int C = {y})"
 
   AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
 
   AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
 
-  AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.   \
-\	            ALL x:domain(g). f`(g`x) = x"
+  AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.   
+	            ALL x:domain(g). f`(g`x) = x"
 
   AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
 
-  AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)   \
-\	            --> (PROD B:A. B)~=0"
+  AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)   
+	            --> (PROD B:A. B)~=0"
 
-  AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)   \
-\	            --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
+  AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)   
+	            --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
 
-  AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->   \
-\	            (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
+  AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->   
+	            (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
 
-  AC10_def "AC10(n) ==  ALL A. (ALL B:A. ~Finite(B)) -->   \
-\	            (EX f. ALL B:A. (pairwise_disjoint(f`B) &   \
-\	            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
+  AC10_def "AC10(n) ==  ALL A. (ALL B:A. ~Finite(B)) -->   
+	            (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
+	            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
 
   AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
 
-  AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->   \
-\	    (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   \
-\	    sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
+  AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->   
+	    (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
+	    sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
 
-  AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &   \
-\	                                  f`B <= B & f`B lepoll m)"
+  AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &   
+	                                  f`B <= B & f`B lepoll m)"
 
   AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
 
-  AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.   \
-\	                              f`B~=0 & f`B <= B & f`B lepoll m))"
+  AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.   
+	                              f`B~=0 & f`B <= B & f`B lepoll m))"
 
-  AC16_def "AC16(n, k)  == ALL A. ~Finite(A) -->   \
-\	    (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   \
-\	    (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
+  AC16_def "AC16(n, k)  == ALL A. ~Finite(A) -->   
+	    (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   
+	    (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
 
-  AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.   \
-\	            EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
+  AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.   
+	            EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
 
-  AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->   \
-\                 ((INT a:A. UN b:B(a). X(a,b)) =   \
-\                 (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
+  AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->   
+                 ((INT a:A. UN b:B(a). X(a,b)) =   
+                 (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
 
-  AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =   \
-\	            (UN f:(PROD B:A. B). INT a:A. f`a))"
+  AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =   
+	            (UN f:(PROD B:A. B). INT a:A. f`a))"
 
 (* Auxiliary definitions used in the above definitions *)
 
-  pairwise_disjoint_def    "pairwise_disjoint(A)   \
-\			    == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
+  pairwise_disjoint_def    "pairwise_disjoint(A)   
+			    == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
 
-  sets_of_size_between_def "sets_of_size_between(A,m,n)   \
-\			    == ALL B:A. m lepoll B & B lepoll n"
+  sets_of_size_between_def "sets_of_size_between(A,m,n)   
+			    == ALL B:A. m lepoll B & B lepoll n"
   
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/HH.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -16,8 +16,8 @@
 
 defs
 
-  HH_def  "HH(f,x,a)  == transrec(a, %b r. (lam z:Pow(x).   \
-\	                 if(f`z:Pow(z)-{0}, f`z, {x}))`(x - (UN c:b. r`c)))"
+  HH_def  "HH(f,x,a)  == transrec(a, %b r. (lam z:Pow(x).   
+	                 if(f`z:Pow(z)-{0}, f`z, {x}))`(x - (UN c:b. r`c)))"
 
 end
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/Transrec2.thy
--- a/src/ZF/AC/Transrec2.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/Transrec2.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -14,10 +14,10 @@
 
 defs
 
-  transrec2_def  "transrec2(alpha, a, b) ==   			\
-\		         transrec(alpha, %i r. if(i=0,   	\
-\		                  a, if(EX j. i=succ(j),   	\
-\		                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   \
-\		                  UN j<i. r`j)))"
+  transrec2_def  "transrec2(alpha, a, b) ==   			
+		         transrec(alpha, %i r. if(i=0,   	
+		                  a, if(EX j. i=succ(j),   	
+		                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
+		                  UN j<i. r`j)))"
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/WO1_AC1.thy
--- a/src/ZF/AC/WO1_AC1.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/WO1_AC1.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -1,3 +1,3 @@
 (*Dummy theory to document dependencies *)
 
-WO1_AC1 = AC_Equiv + WO_AC
\ No newline at end of file
+WO1_AC1 = AC_Equiv + WO_AC
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/WO6_WO1.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -19,19 +19,19 @@
 
 defs
 
-  NN_def  "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a  &  \
-\			    (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
+  NN_def  "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a  &  
+			    (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
 
   uu_def  "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
 
   (*Definitions for case 1*)
 
-  vv1_def "vv1(f,m,b) ==   						\
-\   	   let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &	\
-\	                           domain(uu(f,b,g,d)) lepoll m));   	\
-\	       d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &   		\
-\                           domain(uu(f,b,g,d)) lepoll m		\
-\	   in  if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
+  vv1_def "vv1(f,m,b) ==   						
+   	   let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &	
+	                           domain(uu(f,b,g,d)) lepoll m));   	
+	       d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &   		
+                           domain(uu(f,b,g,d)) lepoll m		
+	   in  if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
 
   ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
 
@@ -39,8 +39,8 @@
   
   (*Definitions for case 2*)
 
-  vv2_def "vv2(f,b,g,s) ==   \
-\	   if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
+  vv2_def "vv2(f,b,g,s) ==   
+	   if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
 
   ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/WO_AC.thy
--- a/src/ZF/AC/WO_AC.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/WO_AC.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -1,3 +1,2 @@
 (*Dummy theory to document dependencies *)
-
-WO_AC = Order + first
\ No newline at end of file
+WO_AC = Order + first
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/first.thy
--- a/src/ZF/AC/first.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/first.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -14,10 +14,10 @@
 
 defs
 
-  first_def                "first(u, X, R)   \
-\			    == u:X & (ALL v:X. v~=u --> <u,v> : R)"
+  first_def                "first(u, X, R)
+ 			    == u:X & (ALL v:X. v~=u --> <u,v> : R)"
 
-  exists_first_def         "exists_first(X,R)   \
-\			    == EX u:X. first(u, X, R)"
+  exists_first_def         "exists_first(X,R)
+ 			    == EX u:X. first(u, X, R)"
 
 end
\ No newline at end of file
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/CardinalArith.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -25,16 +25,16 @@
   cmult_def    "i |*| j == |i*j|"
 
   csquare_rel_def
-  "csquare_rel(K) ==   \
-\        rvimage(K*K,   \
-\                lam <x,y>:K*K. <x Un y, x, y>, \
-\                rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
+  "csquare_rel(K) ==   
+        rvimage(K*K,   
+                lam <x,y>:K*K. <x Un y, x, y>, 
+                rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
 
   (*This def is more complex than Kunen's but it more easily proved to
     be a cardinal*)
   jump_cardinal_def
-      "jump_cardinal(K) ==   \
-\         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
+      "jump_cardinal(K) ==   
+         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
 
   (*needed because jump_cardinal(K) might not be the successor of K*)
   csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Coind/BCR.thy
--- a/src/ZF/Coind/BCR.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/BCR.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -19,9 +19,9 @@
 consts
   isofenv :: "[i,i] => o"
 defs
-  isofenv_def "isofenv(ve,te) ==   		\
-\   ve_dom(ve) = te_dom(te) &   		\
-\   ( ALL x:ve_dom(ve).   			\
-\     EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
+  isofenv_def "isofenv(ve,te) ==   		
+   ve_dom(ve) = te_dom(te) &   		
+   ( ALL x:ve_dom(ve).   			
+     EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
   
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Coind/Dynamic.thy
--- a/src/ZF/Coind/Dynamic.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/Dynamic.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -12,29 +12,29 @@
   domains "EvalRel" <= "ValEnv * Exp * Val"
   intrs
     eval_constI
-      " [| ve:ValEnv; c:Const |] ==>   \
-\       <ve,e_const(c),v_const(c)>:EvalRel"
+      " [| ve:ValEnv; c:Const |] ==>   
+       <ve,e_const(c),v_const(c)>:EvalRel"
     eval_varI
-      " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==>   \
-\       <ve,e_var(x),ve_app(ve,x)>:EvalRel" 
+      " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==>   
+       <ve,e_var(x),ve_app(ve,x)>:EvalRel" 
     eval_fnI
-      " [| ve:ValEnv; x:ExVar; e:Exp |] ==>   \
-\       <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "  
+      " [| ve:ValEnv; x:ExVar; e:Exp |] ==>   
+       <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "  
     eval_fixI
-      " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;   \
-\          v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>   \
-\       <ve,e_fix(f,x,e),cl>:EvalRel " 
+      " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;   
+          v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>   
+       <ve,e_fix(f,x,e),cl>:EvalRel " 
     eval_appI1
-      " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   \
-\          <ve,e1,v_const(c1)>:EvalRel;   \
-\          <ve,e2,v_const(c2)>:EvalRel |] ==>   \
-\       <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
+      " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   
+          <ve,e1,v_const(c1)>:EvalRel;   
+          <ve,e2,v_const(c2)>:EvalRel |] ==>   
+       <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
     eval_appI2
-      " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;   \
-\          <ve,e1,v_clos(xm,em,vem)>:EvalRel;   \
-\          <ve,e2,v2>:EvalRel;   \
-\          <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>   \
-\       <ve,e_app(e1,e2),v>:EvalRel "
+      " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;   
+          <ve,e1,v_clos(xm,em,vem)>:EvalRel;   
+          <ve,e2,v2>:EvalRel;   
+          <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>   
+       <ve,e_app(e1,e2),v>:EvalRel "
   type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs"
 
   
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Coind/ECR.thy
--- a/src/ZF/Coind/ECR.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/ECR.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -16,12 +16,12 @@
     htr_constI
       "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
     htr_closI
-      "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
-\	  <te,e_fn(x,e),t>:ElabRel;  \
-\	  ve_dom(ve) = te_dom(te);   \
-\	  {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  \
-\      |] ==>   \
-\      <v_clos(x,e,ve),t>:HasTyRel" 
+      "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; 
+	  <te,e_fn(x,e),t>:ElabRel;  
+	  ve_dom(ve) = te_dom(te);   
+	  {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
+      |] ==>   
+      <v_clos(x,e,ve),t>:HasTyRel" 
   monos "[Pow_mono]"
   type_intrs "Val_ValEnv.intrs"
   
@@ -31,8 +31,8 @@
   hastyenv :: "[i,i] => o"
 defs
   hastyenv_def 
-    " hastyenv(ve,te) == 			\
-\     ve_dom(ve) = te_dom(te) & 		\
-\     (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
+    " hastyenv(ve,te) == 			
+     ve_dom(ve) = te_dom(te) & 		
+     (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Coind/MT.thy
--- a/src/ZF/Coind/MT.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/MT.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -1,1 +1,1 @@
-MT = ECR
\ No newline at end of file
+MT = ECR
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Coind/Static.thy
--- a/src/ZF/Coind/Static.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/Static.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -12,24 +12,24 @@
   domains "ElabRel" <= "TyEnv * Exp * Ty"
   intrs
     elab_constI
-      " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>   \
-\       <te,e_const(c),t>:ElabRel "
+      " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>   
+       <te,e_const(c),t>:ElabRel "
     elab_varI
-      " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>   \
-\       <te,e_var(x),te_app(te,x)>:ElabRel "
+      " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>   
+       <te,e_var(x),te_app(te,x)>:ElabRel "
     elab_fnI
-      " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;   \
-\          <te_owr(te,x,t1),e,t2>:ElabRel |] ==>   \
-\       <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
+      " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;   
+          <te_owr(te,x,t1),e,t2>:ElabRel |] ==>   
+       <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
     elab_fixI
-      " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;   \
-\          <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>   \
-\       <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
+      " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;   
+          <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>   
+       <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
     elab_appI
-      " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;   \
-\          <te,e1,t_fun(t1,t2)>:ElabRel;   \
-\          <te,e2,t1>:ElabRel |] ==>   \
-\       <te,e_app(e1,e2),t2>:ElabRel "
+      " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;   
+          <te,e1,t_fun(t1,t2)>:ElabRel;   
+          <te,e2,t1>:ElabRel |] ==>   
+       <te,e_app(e1,e2),t2>:ElabRel "
   type_intrs "te_appI::Exp.intrs@Ty.intrs"
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Coind/Types.thy
--- a/src/ZF/Coind/Types.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/Types.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -26,8 +26,8 @@
   te_rec :: "[i,i,[i,i,i,i]=>i] => i"
 defs
   te_rec_def
-    "te_rec(te,c,h) ==   \
-\    Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
+    "te_rec(te,c,h) ==   
+    Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
   
 consts
   te_dom :: "i => i"
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/Values.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -26,8 +26,8 @@
 defs
   ve_emp_def "ve_emp == ve_mk(map_emp)"
   ve_owr_def
-    "ve_owr(ve,x,v) ==   \
-\    ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
+    "ve_owr(ve,x,v) ==   
+    ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
   ve_dom_def
     "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m.domain(m),ve)"
   ve_app_def
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/EquivClass.thy
--- a/src/ZF/EquivClass.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/EquivClass.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -17,7 +17,7 @@
     congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
 
     congruent2_def
-       "congruent2(r,b) == ALL y1 z1 y2 z2. \
-\           <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
+       "congruent2(r,b) == ALL y1 z1 y2 z2. 
+           <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Finite.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -23,7 +23,7 @@
   domains   "FiniteFun(A,B)" <= "Fin(A*B)"
   intrs
     emptyI  "0 : A -||> B"
-    consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   \
-\	     |] ==> cons(<a,b>,h) : A -||> B"
+    consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   
+	     |] ==> cons(<a,b>,h) : A -||> B"
   type_intrs "Fin.intrs"
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/IMP/Com.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -32,8 +32,8 @@
     N   "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
     X  	"[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
     Op1 "[| <e,sigma> -a-> n;  f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
-    Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] \
-\           ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
+    Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] 
+           ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
 
   type_intrs "aexp.intrs@[apply_funtype]"
 
@@ -62,16 +62,16 @@
   intrs (*avoid clash with ML constructors true, false*)
     tru   "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
     fls   "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
-    ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] \
-\	   ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
+    ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] 
+	   ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
     noti  "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
-    andi  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
-\          ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
-    ori   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
-\	    ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
+    andi  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
+          ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
+    ori   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
+	    ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
 
-  type_intrs "bexp.intrs @   \
-\	      [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
+  type_intrs "bexp.intrs @   
+	      [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
   type_elims "[make_elim(evala.dom_subset RS subsetD)]"
 
 
@@ -104,30 +104,30 @@
   intrs
     skip    "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma"
 
-    assign  "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \
-\            <x := a,sigma> -c-> sigma[m/x]"
+    assign  "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> 
+            <x := a,sigma> -c-> sigma[m/x]"
 
-    semi    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \
-\            <c0 ; c1, sigma> -c-> sigma1"
+    semi    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> 
+            <c0 ; c1, sigma> -c-> sigma1"
 
-    ifc1     "[| b:bexp; c1:com; sigma:loc->nat;   \
-\		 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
-\             <ifc b then c0 else c1, sigma> -c-> sigma1"
+    ifc1     "[| b:bexp; c1:com; sigma:loc->nat;   
+		 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> 
+             <ifc b then c0 else c1, sigma> -c-> sigma1"
 
-    ifc0     "[| b:bexp; c0:com; sigma:loc->nat;   \
-\		 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \
-\             <ifc b then c0 else c1, sigma> -c-> sigma1"
+    ifc0     "[| b:bexp; c0:com; sigma:loc->nat;   
+		 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> 
+             <ifc b then c0 else c1, sigma> -c-> sigma1"
 
-    while0   "[| c: com; <b, sigma> -b-> 0 |] ==> \
-\             <while b do c,sigma> -c-> sigma "
+    while0   "[| c: com; <b, sigma> -b-> 0 |] ==> 
+             <while b do c,sigma> -c-> sigma "
 
-    while1   "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \
-\                <while b do c, sigma2> -c-> sigma1 |] ==> \
-\             <while b do c, sigma> -c-> sigma1 "
+    while1   "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; 
+                <while b do c, sigma2> -c-> sigma1 |] ==> 
+             <while b do c, sigma> -c-> sigma1 "
 
   con_defs   "[assign_def]"
   type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
-  type_elims "[make_elim(evala.dom_subset RS subsetD),   \
-\	      make_elim(evalb.dom_subset RS subsetD) ]"
+  type_elims "[make_elim(evala.dom_subset RS subsetD),   
+	      make_elim(evalb.dom_subset RS subsetD) ]"
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/IMP/Denotation.thy
--- a/src/ZF/IMP/Denotation.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/IMP/Denotation.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -31,15 +31,15 @@
   B_or_def	"B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
 
   C_skip_def	"C(skip) == id(loc->nat)"
-  C_assign_def	"C(x := a) == {io:(loc->nat)*(loc->nat). \
-\			       snd(io) = fst(io)[A(a,fst(io))/x]}"
+  C_assign_def	"C(x := a) == {io:(loc->nat)*(loc->nat). 
+			       snd(io) = fst(io)[A(a,fst(io))/x]}"
 
   C_comp_def	"C(c0 ; c1) == C(c1) O C(c0)"
-  C_if_def	"C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un \
-\			 	             {io:C(c1). B(b,fst(io))=0}"
+  C_if_def	"C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un 
+			 	             {io:C(c1). B(b,fst(io))=0}"
 
-  Gamma_def	"Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un \
-\			 	     {io : id(loc->nat). B(b,fst(io))=0})"
+  Gamma_def	"Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un 
+			 	     {io : id(loc->nat). B(b,fst(io))=0})"
 
   C_while_def	"C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Nat.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -20,7 +20,7 @@
 	"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
 
     nat_rec_def
-	"nat_rec(k,a,b) ==   \
-\   	  wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
+	"nat_rec(k,a,b) ==   
+   	  wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Order.thy
--- a/src/ZF/Order.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Order.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -25,17 +25,17 @@
 
   well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
 
-  mono_map_def "mono_map(A,r,B,s) == \
-\                   {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
+  mono_map_def "mono_map(A,r,B,s) == 
+                   {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
 
-  ord_iso_def  "ord_iso(A,r,B,s) == \
-\                   {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
+  ord_iso_def  "ord_iso(A,r,B,s) == 
+                   {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
 
   pred_def     "pred(A,x,r) == {y:A. <y,x>:r}"
 
   ord_iso_map_def
-     "ord_iso_map(A,r,B,s) == \
-\       UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s).   \
-\            {<x,y>}"
+     "ord_iso_map(A,r,B,s) == 
+       UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s).   
+            {<x,y>}"
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/OrderArith.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -13,17 +13,17 @@
 
 defs
   (*disjoint sum of two relations; underlies ordinal addition*)
-  radd_def "radd(A,r,B,s) == \
-\                {z: (A+B) * (A+B).  \
-\                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 \
-\                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 \
-\                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
+  radd_def "radd(A,r,B,s) == 
+                {z: (A+B) * (A+B).  
+                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 
+                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 
+                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
 
   (*lexicographic product of two relations; underlies ordinal multiplication*)
-  rmult_def "rmult(A,r,B,s) == \
-\                {z: (A*B) * (A*B).  \
-\                    EX x' y' x y. z = <<x',y'>, <x,y>> &	 \
-\                       (<x',x>: r | (x'=x & <y',y>: s))}"
+  rmult_def "rmult(A,r,B,s) == 
+                {z: (A*B) * (A*B).  
+                    EX x' y' x y. z = <<x',y'>, <x,y>> &	 
+                       (<x',x>: r | (x'=x & <y',y>: s))}"
 
   (*inverse image of a relation*)
   rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Perm.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -18,8 +18,8 @@
 defs
 
     (*composition of relations and functions; NOT Suppes's relative product*)
-    comp_def	"r O s == {xz : domain(s)*range(r) . \
-\                  		EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
+    comp_def	"r O s == {xz : domain(s)*range(r) . 
+                  		EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
 
     (*the identity function for A*)
     id_def	"id(A) == (lam x:A. x)"
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Rel.thy
--- a/src/ZF/Rel.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Rel.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -25,8 +25,8 @@
 
   trans_def    "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
 
-  trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. 	\
-\                          <x,y>: r --> <y,z>: r --> <x,z>: r"
+  trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. 	
+                          <x,y>: r --> <y,z>: r --> <x,z>: r"
 
   equiv_def    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Resid/Confluence.thy
--- a/src/ZF/Resid/Confluence.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Confluence.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -12,10 +12,10 @@
   strip		:: "o"
 
 defs
-  confluence_def "confluence(R) ==   \
-\		  ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->   \
-\		                         (EX u.<y,u>:R & <z,u>:R))"
-  strip_def      "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->   \
-\		                         (EX u.(y =1=> u) & (z===>u)))" 
+  confluence_def "confluence(R) ==   
+		  ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->   
+		                         (EX u.<y,u>:R & <z,u>:R))"
+  strip_def      "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->   
+		                         (EX u.(y =1=> u) & (z===>u)))" 
 end
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Redex.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -21,8 +21,8 @@
  
 defs
   redex_rec_def
-   "redex_rec(p,b,c,d) == \
-\   Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),   \
-\                             %n x y.d(n, x, y, g`x, g`y), p))"
+   "redex_rec(p,b,c,d) == 
+   Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),   
+                             %n x y.d(n, x, y, g`x, g`y), p))"
 end
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Resid/Reduction.thy
--- a/src/ZF/Resid/Reduction.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Reduction.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -23,10 +23,10 @@
   intrs
     beta	"[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
     rfun  	"[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
-    apl_l	"[|m2:lambda; m1 -1-> n1|] ==>   \
-\		 	          Apl(m1,m2) -1-> Apl(n1,m2)"
-    apl_r	"[|m1:lambda; m2 -1-> n2|] ==>   \
-\		 	          Apl(m1,m2) -1-> Apl(m1,n2)"
+    apl_l	"[|m2:lambda; m1 -1-> n1|] ==>   
+		 	          Apl(m1,m2) -1-> Apl(n1,m2)"
+    apl_r	"[|m1:lambda; m2 -1-> n2|] ==>   
+		 	          Apl(m1,m2) -1-> Apl(m1,n2)"
   type_intrs	"red_typechecks"
 
 inductive
@@ -40,12 +40,12 @@
 inductive
   domains       "Spar_red1" <= "lambda*lambda"
   intrs
-    beta	"[|m =1=> m';   \
-\		 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
+    beta	"[|m =1=> m';   
+		 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
     rvar	"n:nat==> Var(n) =1=> Var(n)"
     rfun	"[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
-    rapl	"[|m =1=> m';   \
-\		 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
+    rapl	"[|m =1=> m';   
+		 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
   type_intrs	"red_typechecks"
 
   inductive
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Resid/Residuals.thy
--- a/src/ZF/Resid/Residuals.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Residuals.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -20,14 +20,14 @@
   domains       "Sres" <= "redexes*redexes*redexes"
   intrs
     Res_Var	"n:nat ==> residuals(Var(n),Var(n),Var(n))"
-    Res_Fun	"[|residuals(u,v,w)|]==>   \
-\		     residuals(Fun(u),Fun(v),Fun(w))"
-    Res_App	"[|residuals(u1,v1,w1);   \
-\		   residuals(u2,v2,w2); b:bool|]==>   \
-\		 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
-    Res_redex	"[|residuals(u1,v1,w1);   \
-\		   residuals(u2,v2,w2); b:bool|]==>   \
-\		 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
+    Res_Fun	"[|residuals(u,v,w)|]==>   
+		     residuals(Fun(u),Fun(v),Fun(w))"
+    Res_App	"[|residuals(u1,v1,w1);   
+		   residuals(u2,v2,w2); b:bool|]==>   
+		 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
+    Res_redex	"[|residuals(u1,v1,w1);   
+		   residuals(u2,v2,w2); b:bool|]==>   
+		 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
   type_intrs	"[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
 
 rules
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Resid/SubUnion.thy
--- a/src/ZF/Resid/SubUnion.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/SubUnion.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -23,10 +23,10 @@
   intrs
     Sub_Var	"n:nat ==> Var(n)<== Var(n)"
     Sub_Fun	"[|u<== v|]==> Fun(u)<== Fun(v)"
-    Sub_App1	"[|u1<== v1; u2<== v2; b:bool|]==>   \
-\		     App(0,u1,u2)<== App(b,v1,v2)"
-    Sub_App2	"[|u1<== v1; u2<== v2|]==>   \
-\		     App(1,u1,u2)<== App(1,v1,v2)"
+    Sub_App1	"[|u1<== v1; u2<== v2; b:bool|]==>   
+		     App(0,u1,u2)<== App(b,v1,v2)"
+    Sub_App2	"[|u1<== v1; u2<== v2|]==>   
+		     App(1,u1,u2)<== App(1,v1,v2)"
   type_intrs	"redexes.intrs@bool_typechecks"
 
 inductive
@@ -34,8 +34,8 @@
   intrs
     Comp_Var	"n:nat ==> Var(n) ~ Var(n)"
     Comp_Fun	"[|u ~ v|]==> Fun(u) ~ Fun(v)"
-    Comp_App	"[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>   \
-\		     App(b1,u1,u2) ~ App(b2,v1,v2)"
+    Comp_App	"[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>   
+		     App(b1,u1,u2) ~ App(b2,v1,v2)"
   type_intrs	"redexes.intrs@bool_typechecks"
 
 inductive
@@ -43,17 +43,17 @@
   intrs
     Reg_Var	"n:nat ==> regular(Var(n))"
     Reg_Fun	"[|regular(u)|]==> regular(Fun(u))"
-    Reg_App1	"[|regular(Fun(u)); regular(v) \
-\		     |]==>regular(App(1,Fun(u),v))"
-    Reg_App2	"[|regular(u); regular(v) \
-\		     |]==>regular(App(0,u,v))"
+    Reg_App1	"[|regular(Fun(u)); regular(v) 
+		     |]==>regular(App(1,Fun(u),v))"
+    Reg_App2	"[|regular(u); regular(v) 
+		     |]==>regular(App(0,u,v))"
   type_intrs	"redexes.intrs@bool_typechecks"
 
 defs
-  union_def  "u un v == redex_rec(u,   \
-\	 %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),   \
-\      %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),   \
-\%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,   \
-\	                               %c z u. App(b or c, m`z, p`u), t))`v"
+  union_def  "u un v == redex_rec(u,   
+	 %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),   
+      %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),   
+%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,   
+	                               %c z u. App(b or c, m`z, p`u), t))`v"
 end
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Resid/Substitution.thy
--- a/src/ZF/Resid/Substitution.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Substitution.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -17,10 +17,10 @@
   "u/v" == "subst_rec(u,v,0)"
   
 defs
-  lift_rec_def	"lift_rec(r,kg) ==   \
-\		     redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), \
-\		                 %x m.(lam k:nat.Fun(m`(succ(k)))),   \
-\		                 %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
+  lift_rec_def	"lift_rec(r,kg) ==   
+		     redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), 
+		                 %x m.(lam k:nat.Fun(m`(succ(k)))),   
+		                 %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
 
   
 (* subst_rec(u,Var(i),k)     = if k<i then Var(i-1)
@@ -30,15 +30,15 @@
    subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))
 
 *)
-  subst_rec_def	"subst_rec(u,t,kg) ==   \
-\		     redex_rec(t,   \
-\		       %i.(lam r:redexes.lam k:nat.   \
-\		              if(k<i,Var(i#-1),   \
-\		                if(k=i,r,Var(i)))),   \
-\		       %x m.(lam r:redexes.lam k:nat.   \
-\                             Fun(m`(lift(r))`(succ(k)))),   \
-\		       %b x y m p.lam r:redexes.lam k:nat.   \
-\		              App(b,m`r`k,p`r`k))`u`kg"
+  subst_rec_def	"subst_rec(u,t,kg) ==   
+		     redex_rec(t,   
+		       %i.(lam r:redexes.lam k:nat.   
+		              if(k<i,Var(i#-1),   
+		                if(k=i,r,Var(i)))),   
+		       %x m.(lam r:redexes.lam k:nat.   
+                             Fun(m`(lift(r))`(succ(k)))),   
+		       %b x y m p.lam r:redexes.lam k:nat.   
+		              App(b,m`r`k,p`r`k))`u`kg"
 
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Resid/Terms.thy
--- a/src/ZF/Resid/Terms.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/Terms.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -24,9 +24,9 @@
   type_intrs	"redexes.intrs@bool_typechecks"
 
 defs
-  unmark_def	"unmark(u) == redex_rec(u,%i.Var(i),   \
-\		                          %x m.Fun(m),   \
-\		                          %b x y m p.Apl(m,p))"
+  unmark_def	"unmark(u) == redex_rec(u,%i.Var(i),   
+		                          %x m.Fun(m),   
+		                          %b x y m p.Apl(m,p))"
 end
 
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Univ.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -25,8 +25,8 @@
     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
 
     Vrec_def
-   	"Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      \
-\                             H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
+   	"Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
+                             H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
 
     univ_def    "univ(A) == Vfrom(A,nat)"
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/WF.thy
--- a/src/ZF/WF.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/WF.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -23,8 +23,8 @@
   (*r is well-founded relation over A*)
   wf_on_def      "wf_on(A,r) == wf(r Int A*A)"
 
-  is_recfun_def  "is_recfun(r,a,H,f) == \
-\   			(f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
+  is_recfun_def  "is_recfun(r,a,H,f) == 
+   			(f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
 
   the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))"
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ZF.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -159,8 +159,8 @@
   foundation    "A=0 | (EX x:A. ALL y:x. y~:A)"
 
   (*Schema axiom since predicate P is a higher-order variable*)
-  replacement   "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \
-                \        b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
+  replacement   "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> 
+                         b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
 
 defs
 
@@ -214,8 +214,8 @@
   domain_def    "domain(r) == {x. w:r, EX y. w=<x,y>}"
   range_def     "range(r) == domain(converse(r))"
   field_def     "field(r) == domain(r) Un range(r)"
-  function_def	"function(r) == ALL x y. <x,y>:r -->   \
-\		                (ALL y'. <x,y'>:r --> y=y')"
+  function_def	"function(r) == ALL x y. <x,y>:r -->   
+		                (ALL y'. <x,y'>:r --> y=y')"
   image_def     "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
   vimage_def    "r -`` A == converse(r)``A"
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Zorn.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -39,8 +39,8 @@
 inductive
   domains       "TFin(S,next)" <= "Pow(S)"
   intrs
-    nextI	"[| x : TFin(S,next);  next: increasing(S) \
-\                |] ==> next`x : TFin(S,next)"
+    nextI	"[| x : TFin(S,next);  next: increasing(S) 
+                |] ==> next`x : TFin(S,next)"
 
     Pow_UnionI	"Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/Bin.thy
--- a/src/ZF/ex/Bin.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Bin.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -44,8 +44,8 @@
 defs
 
   bin_rec_def
-      "bin_rec(z,a,b,h) == \
-\      Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
+      "bin_rec(z,a,b,h) == 
+      Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
 
   integ_of_bin_def
       "integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
@@ -54,39 +54,39 @@
 
   (*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
   norm_Bcons_def
-      "norm_Bcons(w,b) ==   \
-\       bin_case(cond(b,Bcons(w,b),w), cond(b,w,Bcons(w,b)),   \
-\                %w' x'. Bcons(w,b), w)"
+      "norm_Bcons(w,b) ==   
+       bin_case(cond(b,Bcons(w,b),w), cond(b,w,Bcons(w,b)),   
+                %w' x'. Bcons(w,b), w)"
 
   bin_succ_def
-      "bin_succ(w0) ==   \
-\       bin_rec(w0, Bcons(Plus,1), Plus,   \
-\               %w x r. cond(x, Bcons(r,0), norm_Bcons(w,1)))"
+      "bin_succ(w0) ==   
+       bin_rec(w0, Bcons(Plus,1), Plus,   
+               %w x r. cond(x, Bcons(r,0), norm_Bcons(w,1)))"
 
   bin_pred_def
-      "bin_pred(w0) == \
-\       bin_rec(w0, Minus, Bcons(Minus,0),   \
-\               %w x r. cond(x, norm_Bcons(w,0), Bcons(r,1)))"
+      "bin_pred(w0) == 
+       bin_rec(w0, Minus, Bcons(Minus,0),   
+               %w x r. cond(x, norm_Bcons(w,0), Bcons(r,1)))"
 
   bin_minus_def
-      "bin_minus(w0) == \
-\       bin_rec(w0, Plus, Bcons(Plus,1),   \
-\               %w x r. cond(x, bin_pred(Bcons(r,0)), Bcons(r,0)))"
+      "bin_minus(w0) == 
+       bin_rec(w0, Plus, Bcons(Plus,1),   
+               %w x r. cond(x, bin_pred(Bcons(r,0)), Bcons(r,0)))"
 
   bin_add_def
-      "bin_add(v0,w0) ==                        \
-\       bin_rec(v0,                             \
-\         lam w:bin. w,                 \
-\         lam w:bin. bin_pred(w),       \
-\         %v x r. lam w1:bin.           \
-\                  bin_rec(w1, Bcons(v,x), bin_pred(Bcons(v,x)),    \
-\                    %w y s. norm_Bcons(r`cond(x and y, bin_succ(w), w), \
-\                                          x xor y)))    ` w0"
+      "bin_add(v0,w0) ==                        
+       bin_rec(v0,                             
+         lam w:bin. w,                 
+         lam w:bin. bin_pred(w),       
+         %v x r. lam w1:bin.           
+                  bin_rec(w1, Bcons(v,x), bin_pred(Bcons(v,x)),    
+                    %w y s. norm_Bcons(r`cond(x and y, bin_succ(w), w), 
+                                          x xor y)))    ` w0"
 
   bin_mult_def
-      "bin_mult(v0,w) ==                        \
-\       bin_rec(v0, Plus, bin_minus(w),         \
-\         %v x r. cond(x, bin_add(norm_Bcons(r,0),w), norm_Bcons(r,0)))"
+      "bin_mult(v0,w) ==                        
+       bin_rec(v0, Plus, bin_minus(w),         
+         %v x r. cond(x, bin_add(norm_Bcons(r,0),w), norm_Bcons(r,0)))"
 end
 
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/Brouwer.thy
--- a/src/ZF/ex/Brouwer.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Brouwer.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -22,8 +22,8 @@
 datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
   "Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
   monos	      "[Pi_mono]"
-  type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   \
-\	       @ inf_datatype_intrs"
+  type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   
+	       @ inf_datatype_intrs"
 
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/Comb.thy
--- a/src/ZF/ex/Comb.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Comb.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -73,9 +73,9 @@
 
 defs
 
-  diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
-\                            (ALL y'. <x,y'>:r --> \
-\                                 (EX z. <y,z>:r & <y',z> : r))"
+  diamond_def "diamond(r) == ALL x y. <x,y>:r --> 
+                            (ALL y'. <x,y'>:r --> 
+                                 (EX z. <y,z>:r & <y',z> : r))"
 
   I_def       "I == S#K#K"
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/Integ.thy
--- a/src/ZF/ex/Integ.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Integ.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -23,8 +23,8 @@
 defs
 
     intrel_def
-     "intrel == {p:(nat*nat)*(nat*nat). 		\
-\        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
+     "intrel == {p:(nat*nat)*(nat*nat). 		
+        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
 
     integ_def   "integ == (nat*nat)/intrel"
     
@@ -42,17 +42,17 @@
       Perhaps a "curried" or even polymorphic congruent predicate would be
       better.*)
     zadd_def
-     "Z1 $+ Z2 == \
-\       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 \
-\                           in intrel``{<x1#+x2, y1#+y2>}"
+     "Z1 $+ Z2 == 
+       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
+                           in intrel``{<x1#+x2, y1#+y2>}"
     
     zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
     zless_def	"Z1 $< Z2 == znegative(Z1 $- Z2)"
     
     (*This illustrates the primitive form of definitions (no patterns)*)
     zmult_def
-     "Z1 $* Z2 == \
-\       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        \
-\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
+     "Z1 $* Z2 == 
+       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
+                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
     
  end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/LList.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -49,8 +49,8 @@
 rules
   flip_LNil   "flip(LNil) = LNil"
 
-  flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
-\              flip(LCons(x,l)) = LCons(not(x), flip(l))"
+  flip_LCons  "[| x:bool; l: llist(bool) |] ==> 
+              flip(LCons(x,l)) = LCons(not(x), flip(l))"
 
 end
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/Primrec.thy
--- a/src/ZF/ex/Primrec.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Primrec.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -39,12 +39,12 @@
   COMP_def  "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)"
 
   (*Note that g is applied first to PREC(f,g)`y and then to y!*)
-  PREC_def  "PREC(f,g) == \
-\            lam l:list(nat). list_case(0, \
-\                      %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
+  PREC_def  "PREC(f,g) == 
+            lam l:list(nat). list_case(0, 
+                      %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
   
-  ACK_def   "ACK(i) == rec(i, SC, \
-\                      %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
+  ACK_def   "ACK(i) == rec(i, SC, 
+                      %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
 
 
 inductive
@@ -57,8 +57,8 @@
     PREC     "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
   monos      "[list_mono]"
   con_defs   "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
-  type_intrs "nat_typechecks @ list.intrs @   		        \
-\	      [lam_type, list_case_type, drop_type, map_type,   \
-\	      apply_type, rec_type]"
+  type_intrs "nat_typechecks @ list.intrs @   		        
+	      [lam_type, list_case_type, drop_type, map_type,   
+	      apply_type, rec_type]"
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/PropLog.thy
--- a/src/ZF/ex/PropLog.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/PropLog.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -47,13 +47,13 @@
 defs
 
   prop_rec_def
-   "prop_rec(p,b,c,h) == \
-\   Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
+   "prop_rec(p,b,c,h) == 
+   Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
 
   (** Semantics of propositional logic **)
   is_true_def
-   "is_true(p,t) == prop_rec(p, 0,  %v. if(v:t, 1, 0), \
-\                               %p q tp tq. if(tp=1,tq,1))         =  1"
+   "is_true(p,t) == prop_rec(p, 0,  %v. if(v:t, 1, 0), 
+                               %p q tp tq. if(tp=1,tq,1))         =  1"
 
   (*Logical consequence: for every valuation, if all elements of H are true
      then so is p*)
@@ -61,7 +61,7 @@
 
   (** A finite set of hypotheses from t and the Vars in p **)
   hyps_def
-   "hyps(p,t) == prop_rec(p, 0,  %v. {if(v:t, #v, #v=>Fls)}, \
-\                            %p q Hp Hq. Hp Un Hq)"
+   "hyps(p,t) == prop_rec(p, 0,  %v. {if(v:t, #v, #v=>Fls)}, 
+                            %p q Hp Hq. Hp Un Hq)"
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/Ramsey.thy
--- a/src/ZF/ex/Ramsey.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Ramsey.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -39,8 +39,8 @@
     "Atleast(n,S) == (EX f. f: inj(n,S))"
 
   Ramsey_def
-    "Ramsey(n,i,j) == ALL V E. Symmetric(E) & Atleast(n,V) -->  \
-\         (EX C. Clique(C,V,E) & Atleast(i,C)) |       \
-\         (EX I. Indept(I,V,E) & Atleast(j,I))"
+    "Ramsey(n,i,j) == ALL V E. Symmetric(E) & Atleast(n,V) -->  
+         (EX C. Clique(C,V,E) & Atleast(i,C)) |       
+         (EX I. Indept(I,V,E) & Atleast(j,I))"
 
 end
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/Rmap.thy
--- a/src/ZF/ex/Rmap.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Rmap.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -16,8 +16,8 @@
   intrs
     NilI  "<Nil,Nil> : rmap(r)"
 
-    ConsI "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> \
-\          <Cons(x,xs), Cons(y,ys)> : rmap(r)"
+    ConsI "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> 
+          <Cons(x,xs), Cons(y,ys)> : rmap(r)"
 
   type_intrs "[domainI,rangeI] @ list.intrs"
 
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/TF.thy
--- a/src/ZF/ex/TF.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/TF.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -24,21 +24,21 @@
 
 defs
   TF_rec_def
-    "TF_rec(z,b,c,d) == Vrec(z,  			\
-\      %z r. tree_forest_case(%x f. b(x, f, r`f), 	\
-\                             c, 			\
-\		              %t f. d(t, f, r`t, r`f), z))"
+    "TF_rec(z,b,c,d) == Vrec(z,  			
+      %z r. tree_forest_case(%x f. b(x, f, r`f), 	
+                             c, 			
+		              %t f. d(t, f, r`t, r`f), z))"
 
   list_of_TF_def
-    "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], \
-\		             %t f r1 r2. Cons(t, r2))"
+    "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], 
+		             %t f r1 r2. Cons(t, r2))"
 
   TF_of_list_def
     "TF_of_list(f) == list_rec(f, Fnil,  %t f r. Fcons(t,r))"
 
   TF_map_def
-    "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, \
-\                           %t f r1 r2. Fcons(r1,r2))"
+    "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, 
+                           %t f r1 r2. Fcons(r1,r2))"
 
   TF_size_def
     "TF_size(z) == TF_rec(z, %x f r.succ(r), 0, %t f r1 r2. r1#+r2)"
diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/ex/Term.thy
--- a/src/ZF/ex/Term.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ex/Term.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -28,8 +28,8 @@
 
 defs
   term_rec_def
-   "term_rec(t,d) == \
-\   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
+   "term_rec(t,d) == 
+   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
 
   term_map_def	"term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"