removed \...\ inside strings
authorclasohm
Thu Jun 22 17:13:05 1995 +0200 (1995-06-22)
changeset 1155928a16e02f9f
parent 1154 bc295e3dc078
child 1156 b373cb33352f
removed \...\ inside strings
src/ZF/AC/AC15_WO6.thy
src/ZF/AC/AC17_AC1.thy
src/ZF/AC/AC1_WO2.thy
src/ZF/AC/AC_Equiv.thy
src/ZF/AC/HH.thy
src/ZF/AC/Transrec2.thy
src/ZF/AC/WO1_AC1.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/AC/WO_AC.thy
src/ZF/AC/first.thy
src/ZF/CardinalArith.thy
src/ZF/Coind/BCR.thy
src/ZF/Coind/Dynamic.thy
src/ZF/Coind/ECR.thy
src/ZF/Coind/MT.thy
src/ZF/Coind/Static.thy
src/ZF/Coind/Types.thy
src/ZF/Coind/Values.thy
src/ZF/EquivClass.thy
src/ZF/Finite.thy
src/ZF/IMP/Com.thy
src/ZF/IMP/Denotation.thy
src/ZF/Nat.thy
src/ZF/Order.thy
src/ZF/OrderArith.thy
src/ZF/Perm.thy
src/ZF/Rel.thy
src/ZF/Resid/Confluence.thy
src/ZF/Resid/Redex.thy
src/ZF/Resid/Reduction.thy
src/ZF/Resid/Residuals.thy
src/ZF/Resid/SubUnion.thy
src/ZF/Resid/Substitution.thy
src/ZF/Resid/Terms.thy
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/ZF.thy
src/ZF/Zorn.thy
src/ZF/ex/Bin.thy
src/ZF/ex/Brouwer.thy
src/ZF/ex/Comb.thy
src/ZF/ex/Integ.thy
src/ZF/ex/LList.thy
src/ZF/ex/Primrec.thy
src/ZF/ex/PropLog.thy
src/ZF/ex/Ramsey.thy
src/ZF/ex/Rmap.thy
src/ZF/ex/TF.thy
src/ZF/ex/Term.thy
     1.1 --- a/src/ZF/AC/AC15_WO6.thy	Thu Jun 22 12:58:39 1995 +0200
     1.2 +++ b/src/ZF/AC/AC15_WO6.thy	Thu Jun 22 17:13:05 1995 +0200
     1.3 @@ -1,3 +1,3 @@
     1.4  (*Dummy theory to document dependencies *)
     1.5  
     1.6 -AC15_WO6 = HH
     1.7 \ No newline at end of file
     1.8 +AC15_WO6 = HH
     2.1 --- a/src/ZF/AC/AC17_AC1.thy	Thu Jun 22 12:58:39 1995 +0200
     2.2 +++ b/src/ZF/AC/AC17_AC1.thy	Thu Jun 22 17:13:05 1995 +0200
     2.3 @@ -1,3 +1,3 @@
     2.4  (*Dummy theory to document dependencies *)
     2.5  
     2.6 -AC17_AC1 = HH
     2.7 \ No newline at end of file
     2.8 +AC17_AC1 = HH
     3.1 --- a/src/ZF/AC/AC1_WO2.thy	Thu Jun 22 12:58:39 1995 +0200
     3.2 +++ b/src/ZF/AC/AC1_WO2.thy	Thu Jun 22 17:13:05 1995 +0200
     3.3 @@ -1,3 +1,3 @@
     3.4  (*Dummy theory to document dependencies *)
     3.5  
     3.6 -AC1_WO2 = HH
     3.7 \ No newline at end of file
     3.8 +AC1_WO2 = HH
     4.1 --- a/src/ZF/AC/AC_Equiv.thy	Thu Jun 22 12:58:39 1995 +0200
     4.2 +++ b/src/ZF/AC/AC_Equiv.thy	Thu Jun 22 17:13:05 1995 +0200
     4.3 @@ -41,19 +41,19 @@
     4.4  
     4.5    WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
     4.6  
     4.7 -  WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &   \
     4.8 -\	             (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
     4.9 +  WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &   
    4.10 +	             (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
    4.11  
    4.12    WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
    4.13  
    4.14 -  WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a   \
    4.15 -\	            & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
    4.16 +  WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a   
    4.17 +	            & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
    4.18  
    4.19 -  WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->   \
    4.20 -\	            well_ord(A,converse(R)))"
    4.21 +  WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->   
    4.22 +	            well_ord(A,converse(R)))"
    4.23  
    4.24 -  WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->  \
    4.25 -\	            (EX R. well_ord(A,R))"
    4.26 +  WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->  
    4.27 +	            (EX R. well_ord(A,R))"
    4.28  
    4.29  (* Axioms of Choice *)  
    4.30  
    4.31 @@ -61,65 +61,65 @@
    4.32  
    4.33    AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
    4.34  
    4.35 -  AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)   \
    4.36 -\	            --> (EX C. ALL B:A. EX y. B Int C = {y})"
    4.37 +  AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)   
    4.38 +	            --> (EX C. ALL B:A. EX y. B Int C = {y})"
    4.39  
    4.40    AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
    4.41  
    4.42    AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
    4.43  
    4.44 -  AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.   \
    4.45 -\	            ALL x:domain(g). f`(g`x) = x"
    4.46 +  AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.   
    4.47 +	            ALL x:domain(g). f`(g`x) = x"
    4.48  
    4.49    AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
    4.50  
    4.51 -  AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)   \
    4.52 -\	            --> (PROD B:A. B)~=0"
    4.53 +  AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)   
    4.54 +	            --> (PROD B:A. B)~=0"
    4.55  
    4.56 -  AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)   \
    4.57 -\	            --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
    4.58 +  AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)   
    4.59 +	            --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
    4.60  
    4.61 -  AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->   \
    4.62 -\	            (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
    4.63 +  AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->   
    4.64 +	            (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
    4.65  
    4.66 -  AC10_def "AC10(n) ==  ALL A. (ALL B:A. ~Finite(B)) -->   \
    4.67 -\	            (EX f. ALL B:A. (pairwise_disjoint(f`B) &   \
    4.68 -\	            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
    4.69 +  AC10_def "AC10(n) ==  ALL A. (ALL B:A. ~Finite(B)) -->   
    4.70 +	            (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
    4.71 +	            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
    4.72  
    4.73    AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
    4.74  
    4.75 -  AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->   \
    4.76 -\	    (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   \
    4.77 -\	    sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
    4.78 +  AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->   
    4.79 +	    (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
    4.80 +	    sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
    4.81  
    4.82 -  AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &   \
    4.83 -\	                                  f`B <= B & f`B lepoll m)"
    4.84 +  AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &   
    4.85 +	                                  f`B <= B & f`B lepoll m)"
    4.86  
    4.87    AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
    4.88  
    4.89 -  AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.   \
    4.90 -\	                              f`B~=0 & f`B <= B & f`B lepoll m))"
    4.91 +  AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.   
    4.92 +	                              f`B~=0 & f`B <= B & f`B lepoll m))"
    4.93  
    4.94 -  AC16_def "AC16(n, k)  == ALL A. ~Finite(A) -->   \
    4.95 -\	    (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   \
    4.96 -\	    (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
    4.97 +  AC16_def "AC16(n, k)  == ALL A. ~Finite(A) -->   
    4.98 +	    (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   
    4.99 +	    (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
   4.100  
   4.101 -  AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.   \
   4.102 -\	            EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
   4.103 +  AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.   
   4.104 +	            EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
   4.105  
   4.106 -  AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->   \
   4.107 -\                 ((INT a:A. UN b:B(a). X(a,b)) =   \
   4.108 -\                 (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
   4.109 +  AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->   
   4.110 +                 ((INT a:A. UN b:B(a). X(a,b)) =   
   4.111 +                 (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
   4.112  
   4.113 -  AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =   \
   4.114 -\	            (UN f:(PROD B:A. B). INT a:A. f`a))"
   4.115 +  AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =   
   4.116 +	            (UN f:(PROD B:A. B). INT a:A. f`a))"
   4.117  
   4.118  (* Auxiliary definitions used in the above definitions *)
   4.119  
   4.120 -  pairwise_disjoint_def    "pairwise_disjoint(A)   \
   4.121 -\			    == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
   4.122 +  pairwise_disjoint_def    "pairwise_disjoint(A)   
   4.123 +			    == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
   4.124  
   4.125 -  sets_of_size_between_def "sets_of_size_between(A,m,n)   \
   4.126 -\			    == ALL B:A. m lepoll B & B lepoll n"
   4.127 +  sets_of_size_between_def "sets_of_size_between(A,m,n)   
   4.128 +			    == ALL B:A. m lepoll B & B lepoll n"
   4.129    
   4.130  end
     5.1 --- a/src/ZF/AC/HH.thy	Thu Jun 22 12:58:39 1995 +0200
     5.2 +++ b/src/ZF/AC/HH.thy	Thu Jun 22 17:13:05 1995 +0200
     5.3 @@ -16,8 +16,8 @@
     5.4  
     5.5  defs
     5.6  
     5.7 -  HH_def  "HH(f,x,a)  == transrec(a, %b r. (lam z:Pow(x).   \
     5.8 -\	                 if(f`z:Pow(z)-{0}, f`z, {x}))`(x - (UN c:b. r`c)))"
     5.9 +  HH_def  "HH(f,x,a)  == transrec(a, %b r. (lam z:Pow(x).   
    5.10 +	                 if(f`z:Pow(z)-{0}, f`z, {x}))`(x - (UN c:b. r`c)))"
    5.11  
    5.12  end
    5.13  
     6.1 --- a/src/ZF/AC/Transrec2.thy	Thu Jun 22 12:58:39 1995 +0200
     6.2 +++ b/src/ZF/AC/Transrec2.thy	Thu Jun 22 17:13:05 1995 +0200
     6.3 @@ -14,10 +14,10 @@
     6.4  
     6.5  defs
     6.6  
     6.7 -  transrec2_def  "transrec2(alpha, a, b) ==   			\
     6.8 -\		         transrec(alpha, %i r. if(i=0,   	\
     6.9 -\		                  a, if(EX j. i=succ(j),   	\
    6.10 -\		                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   \
    6.11 -\		                  UN j<i. r`j)))"
    6.12 +  transrec2_def  "transrec2(alpha, a, b) ==   			
    6.13 +		         transrec(alpha, %i r. if(i=0,   	
    6.14 +		                  a, if(EX j. i=succ(j),   	
    6.15 +		                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    6.16 +		                  UN j<i. r`j)))"
    6.17  
    6.18  end
     7.1 --- a/src/ZF/AC/WO1_AC1.thy	Thu Jun 22 12:58:39 1995 +0200
     7.2 +++ b/src/ZF/AC/WO1_AC1.thy	Thu Jun 22 17:13:05 1995 +0200
     7.3 @@ -1,3 +1,3 @@
     7.4  (*Dummy theory to document dependencies *)
     7.5  
     7.6 -WO1_AC1 = AC_Equiv + WO_AC
     7.7 \ No newline at end of file
     7.8 +WO1_AC1 = AC_Equiv + WO_AC
     8.1 --- a/src/ZF/AC/WO6_WO1.thy	Thu Jun 22 12:58:39 1995 +0200
     8.2 +++ b/src/ZF/AC/WO6_WO1.thy	Thu Jun 22 17:13:05 1995 +0200
     8.3 @@ -19,19 +19,19 @@
     8.4  
     8.5  defs
     8.6  
     8.7 -  NN_def  "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a  &  \
     8.8 -\			    (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
     8.9 +  NN_def  "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a  &  
    8.10 +			    (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
    8.11  
    8.12    uu_def  "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
    8.13  
    8.14    (*Definitions for case 1*)
    8.15  
    8.16 -  vv1_def "vv1(f,m,b) ==   						\
    8.17 -\   	   let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &	\
    8.18 -\	                           domain(uu(f,b,g,d)) lepoll m));   	\
    8.19 -\	       d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &   		\
    8.20 -\                           domain(uu(f,b,g,d)) lepoll m		\
    8.21 -\	   in  if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
    8.22 +  vv1_def "vv1(f,m,b) ==   						
    8.23 +   	   let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &	
    8.24 +	                           domain(uu(f,b,g,d)) lepoll m));   	
    8.25 +	       d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &   		
    8.26 +                           domain(uu(f,b,g,d)) lepoll m		
    8.27 +	   in  if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
    8.28  
    8.29    ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
    8.30  
    8.31 @@ -39,8 +39,8 @@
    8.32    
    8.33    (*Definitions for case 2*)
    8.34  
    8.35 -  vv2_def "vv2(f,b,g,s) ==   \
    8.36 -\	   if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
    8.37 +  vv2_def "vv2(f,b,g,s) ==   
    8.38 +	   if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
    8.39  
    8.40    ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
    8.41  
     9.1 --- a/src/ZF/AC/WO_AC.thy	Thu Jun 22 12:58:39 1995 +0200
     9.2 +++ b/src/ZF/AC/WO_AC.thy	Thu Jun 22 17:13:05 1995 +0200
     9.3 @@ -1,3 +1,2 @@
     9.4  (*Dummy theory to document dependencies *)
     9.5 -
     9.6 -WO_AC = Order + first
     9.7 \ No newline at end of file
     9.8 +WO_AC = Order + first
    10.1 --- a/src/ZF/AC/first.thy	Thu Jun 22 12:58:39 1995 +0200
    10.2 +++ b/src/ZF/AC/first.thy	Thu Jun 22 17:13:05 1995 +0200
    10.3 @@ -14,10 +14,10 @@
    10.4  
    10.5  defs
    10.6  
    10.7 -  first_def                "first(u, X, R)   \
    10.8 -\			    == u:X & (ALL v:X. v~=u --> <u,v> : R)"
    10.9 +  first_def                "first(u, X, R)
   10.10 + 			    == u:X & (ALL v:X. v~=u --> <u,v> : R)"
   10.11  
   10.12 -  exists_first_def         "exists_first(X,R)   \
   10.13 -\			    == EX u:X. first(u, X, R)"
   10.14 +  exists_first_def         "exists_first(X,R)
   10.15 + 			    == EX u:X. first(u, X, R)"
   10.16  
   10.17  end
   10.18 \ No newline at end of file
    11.1 --- a/src/ZF/CardinalArith.thy	Thu Jun 22 12:58:39 1995 +0200
    11.2 +++ b/src/ZF/CardinalArith.thy	Thu Jun 22 17:13:05 1995 +0200
    11.3 @@ -25,16 +25,16 @@
    11.4    cmult_def    "i |*| j == |i*j|"
    11.5  
    11.6    csquare_rel_def
    11.7 -  "csquare_rel(K) ==   \
    11.8 -\        rvimage(K*K,   \
    11.9 -\                lam <x,y>:K*K. <x Un y, x, y>, \
   11.10 -\                rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
   11.11 +  "csquare_rel(K) ==   
   11.12 +        rvimage(K*K,   
   11.13 +                lam <x,y>:K*K. <x Un y, x, y>, 
   11.14 +                rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
   11.15  
   11.16    (*This def is more complex than Kunen's but it more easily proved to
   11.17      be a cardinal*)
   11.18    jump_cardinal_def
   11.19 -      "jump_cardinal(K) ==   \
   11.20 -\         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
   11.21 +      "jump_cardinal(K) ==   
   11.22 +         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
   11.23  
   11.24    (*needed because jump_cardinal(K) might not be the successor of K*)
   11.25    csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
    12.1 --- a/src/ZF/Coind/BCR.thy	Thu Jun 22 12:58:39 1995 +0200
    12.2 +++ b/src/ZF/Coind/BCR.thy	Thu Jun 22 17:13:05 1995 +0200
    12.3 @@ -19,9 +19,9 @@
    12.4  consts
    12.5    isofenv :: "[i,i] => o"
    12.6  defs
    12.7 -  isofenv_def "isofenv(ve,te) ==   		\
    12.8 -\   ve_dom(ve) = te_dom(te) &   		\
    12.9 -\   ( ALL x:ve_dom(ve).   			\
   12.10 -\     EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
   12.11 +  isofenv_def "isofenv(ve,te) ==   		
   12.12 +   ve_dom(ve) = te_dom(te) &   		
   12.13 +   ( ALL x:ve_dom(ve).   			
   12.14 +     EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
   12.15    
   12.16  end
    13.1 --- a/src/ZF/Coind/Dynamic.thy	Thu Jun 22 12:58:39 1995 +0200
    13.2 +++ b/src/ZF/Coind/Dynamic.thy	Thu Jun 22 17:13:05 1995 +0200
    13.3 @@ -12,29 +12,29 @@
    13.4    domains "EvalRel" <= "ValEnv * Exp * Val"
    13.5    intrs
    13.6      eval_constI
    13.7 -      " [| ve:ValEnv; c:Const |] ==>   \
    13.8 -\       <ve,e_const(c),v_const(c)>:EvalRel"
    13.9 +      " [| ve:ValEnv; c:Const |] ==>   
   13.10 +       <ve,e_const(c),v_const(c)>:EvalRel"
   13.11      eval_varI
   13.12 -      " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==>   \
   13.13 -\       <ve,e_var(x),ve_app(ve,x)>:EvalRel" 
   13.14 +      " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==>   
   13.15 +       <ve,e_var(x),ve_app(ve,x)>:EvalRel" 
   13.16      eval_fnI
   13.17 -      " [| ve:ValEnv; x:ExVar; e:Exp |] ==>   \
   13.18 -\       <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "  
   13.19 +      " [| ve:ValEnv; x:ExVar; e:Exp |] ==>   
   13.20 +       <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "  
   13.21      eval_fixI
   13.22 -      " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;   \
   13.23 -\          v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>   \
   13.24 -\       <ve,e_fix(f,x,e),cl>:EvalRel " 
   13.25 +      " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;   
   13.26 +          v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>   
   13.27 +       <ve,e_fix(f,x,e),cl>:EvalRel " 
   13.28      eval_appI1
   13.29 -      " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   \
   13.30 -\          <ve,e1,v_const(c1)>:EvalRel;   \
   13.31 -\          <ve,e2,v_const(c2)>:EvalRel |] ==>   \
   13.32 -\       <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
   13.33 +      " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   
   13.34 +          <ve,e1,v_const(c1)>:EvalRel;   
   13.35 +          <ve,e2,v_const(c2)>:EvalRel |] ==>   
   13.36 +       <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
   13.37      eval_appI2
   13.38 -      " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;   \
   13.39 -\          <ve,e1,v_clos(xm,em,vem)>:EvalRel;   \
   13.40 -\          <ve,e2,v2>:EvalRel;   \
   13.41 -\          <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>   \
   13.42 -\       <ve,e_app(e1,e2),v>:EvalRel "
   13.43 +      " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;   
   13.44 +          <ve,e1,v_clos(xm,em,vem)>:EvalRel;   
   13.45 +          <ve,e2,v2>:EvalRel;   
   13.46 +          <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>   
   13.47 +       <ve,e_app(e1,e2),v>:EvalRel "
   13.48    type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs"
   13.49  
   13.50    
    14.1 --- a/src/ZF/Coind/ECR.thy	Thu Jun 22 12:58:39 1995 +0200
    14.2 +++ b/src/ZF/Coind/ECR.thy	Thu Jun 22 17:13:05 1995 +0200
    14.3 @@ -16,12 +16,12 @@
    14.4      htr_constI
    14.5        "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
    14.6      htr_closI
    14.7 -      "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
    14.8 -\	  <te,e_fn(x,e),t>:ElabRel;  \
    14.9 -\	  ve_dom(ve) = te_dom(te);   \
   14.10 -\	  {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  \
   14.11 -\      |] ==>   \
   14.12 -\      <v_clos(x,e,ve),t>:HasTyRel" 
   14.13 +      "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; 
   14.14 +	  <te,e_fn(x,e),t>:ElabRel;  
   14.15 +	  ve_dom(ve) = te_dom(te);   
   14.16 +	  {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
   14.17 +      |] ==>   
   14.18 +      <v_clos(x,e,ve),t>:HasTyRel" 
   14.19    monos "[Pow_mono]"
   14.20    type_intrs "Val_ValEnv.intrs"
   14.21    
   14.22 @@ -31,8 +31,8 @@
   14.23    hastyenv :: "[i,i] => o"
   14.24  defs
   14.25    hastyenv_def 
   14.26 -    " hastyenv(ve,te) == 			\
   14.27 -\     ve_dom(ve) = te_dom(te) & 		\
   14.28 -\     (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
   14.29 +    " hastyenv(ve,te) == 			
   14.30 +     ve_dom(ve) = te_dom(te) & 		
   14.31 +     (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
   14.32  
   14.33  end
    15.1 --- a/src/ZF/Coind/MT.thy	Thu Jun 22 12:58:39 1995 +0200
    15.2 +++ b/src/ZF/Coind/MT.thy	Thu Jun 22 17:13:05 1995 +0200
    15.3 @@ -1,1 +1,1 @@
    15.4 -MT = ECR
    15.5 \ No newline at end of file
    15.6 +MT = ECR
    16.1 --- a/src/ZF/Coind/Static.thy	Thu Jun 22 12:58:39 1995 +0200
    16.2 +++ b/src/ZF/Coind/Static.thy	Thu Jun 22 17:13:05 1995 +0200
    16.3 @@ -12,24 +12,24 @@
    16.4    domains "ElabRel" <= "TyEnv * Exp * Ty"
    16.5    intrs
    16.6      elab_constI
    16.7 -      " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>   \
    16.8 -\       <te,e_const(c),t>:ElabRel "
    16.9 +      " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>   
   16.10 +       <te,e_const(c),t>:ElabRel "
   16.11      elab_varI
   16.12 -      " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>   \
   16.13 -\       <te,e_var(x),te_app(te,x)>:ElabRel "
   16.14 +      " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>   
   16.15 +       <te,e_var(x),te_app(te,x)>:ElabRel "
   16.16      elab_fnI
   16.17 -      " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;   \
   16.18 -\          <te_owr(te,x,t1),e,t2>:ElabRel |] ==>   \
   16.19 -\       <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
   16.20 +      " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;   
   16.21 +          <te_owr(te,x,t1),e,t2>:ElabRel |] ==>   
   16.22 +       <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
   16.23      elab_fixI
   16.24 -      " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;   \
   16.25 -\          <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>   \
   16.26 -\       <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
   16.27 +      " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;   
   16.28 +          <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>   
   16.29 +       <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
   16.30      elab_appI
   16.31 -      " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;   \
   16.32 -\          <te,e1,t_fun(t1,t2)>:ElabRel;   \
   16.33 -\          <te,e2,t1>:ElabRel |] ==>   \
   16.34 -\       <te,e_app(e1,e2),t2>:ElabRel "
   16.35 +      " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;   
   16.36 +          <te,e1,t_fun(t1,t2)>:ElabRel;   
   16.37 +          <te,e2,t1>:ElabRel |] ==>   
   16.38 +       <te,e_app(e1,e2),t2>:ElabRel "
   16.39    type_intrs "te_appI::Exp.intrs@Ty.intrs"
   16.40  
   16.41  end
    17.1 --- a/src/ZF/Coind/Types.thy	Thu Jun 22 12:58:39 1995 +0200
    17.2 +++ b/src/ZF/Coind/Types.thy	Thu Jun 22 17:13:05 1995 +0200
    17.3 @@ -26,8 +26,8 @@
    17.4    te_rec :: "[i,i,[i,i,i,i]=>i] => i"
    17.5  defs
    17.6    te_rec_def
    17.7 -    "te_rec(te,c,h) ==   \
    17.8 -\    Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
    17.9 +    "te_rec(te,c,h) ==   
   17.10 +    Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
   17.11    
   17.12  consts
   17.13    te_dom :: "i => i"
    18.1 --- a/src/ZF/Coind/Values.thy	Thu Jun 22 12:58:39 1995 +0200
    18.2 +++ b/src/ZF/Coind/Values.thy	Thu Jun 22 17:13:05 1995 +0200
    18.3 @@ -26,8 +26,8 @@
    18.4  defs
    18.5    ve_emp_def "ve_emp == ve_mk(map_emp)"
    18.6    ve_owr_def
    18.7 -    "ve_owr(ve,x,v) ==   \
    18.8 -\    ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
    18.9 +    "ve_owr(ve,x,v) ==   
   18.10 +    ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
   18.11    ve_dom_def
   18.12      "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m.domain(m),ve)"
   18.13    ve_app_def
    19.1 --- a/src/ZF/EquivClass.thy	Thu Jun 22 12:58:39 1995 +0200
    19.2 +++ b/src/ZF/EquivClass.thy	Thu Jun 22 17:13:05 1995 +0200
    19.3 @@ -17,7 +17,7 @@
    19.4      congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
    19.5  
    19.6      congruent2_def
    19.7 -       "congruent2(r,b) == ALL y1 z1 y2 z2. \
    19.8 -\           <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
    19.9 +       "congruent2(r,b) == ALL y1 z1 y2 z2. 
   19.10 +           <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
   19.11  
   19.12  end
    20.1 --- a/src/ZF/Finite.thy	Thu Jun 22 12:58:39 1995 +0200
    20.2 +++ b/src/ZF/Finite.thy	Thu Jun 22 17:13:05 1995 +0200
    20.3 @@ -23,7 +23,7 @@
    20.4    domains   "FiniteFun(A,B)" <= "Fin(A*B)"
    20.5    intrs
    20.6      emptyI  "0 : A -||> B"
    20.7 -    consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   \
    20.8 -\	     |] ==> cons(<a,b>,h) : A -||> B"
    20.9 +    consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   
   20.10 +	     |] ==> cons(<a,b>,h) : A -||> B"
   20.11    type_intrs "Fin.intrs"
   20.12  end
    21.1 --- a/src/ZF/IMP/Com.thy	Thu Jun 22 12:58:39 1995 +0200
    21.2 +++ b/src/ZF/IMP/Com.thy	Thu Jun 22 17:13:05 1995 +0200
    21.3 @@ -32,8 +32,8 @@
    21.4      N   "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
    21.5      X  	"[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
    21.6      Op1 "[| <e,sigma> -a-> n;  f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
    21.7 -    Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] \
    21.8 -\           ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
    21.9 +    Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] 
   21.10 +           ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
   21.11  
   21.12    type_intrs "aexp.intrs@[apply_funtype]"
   21.13  
   21.14 @@ -62,16 +62,16 @@
   21.15    intrs (*avoid clash with ML constructors true, false*)
   21.16      tru   "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
   21.17      fls   "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
   21.18 -    ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] \
   21.19 -\	   ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
   21.20 +    ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] 
   21.21 +	   ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
   21.22      noti  "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
   21.23 -    andi  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
   21.24 -\          ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
   21.25 -    ori   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
   21.26 -\	    ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
   21.27 +    andi  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
   21.28 +          ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
   21.29 +    ori   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
   21.30 +	    ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
   21.31  
   21.32 -  type_intrs "bexp.intrs @   \
   21.33 -\	      [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
   21.34 +  type_intrs "bexp.intrs @   
   21.35 +	      [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
   21.36    type_elims "[make_elim(evala.dom_subset RS subsetD)]"
   21.37  
   21.38  
   21.39 @@ -104,30 +104,30 @@
   21.40    intrs
   21.41      skip    "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma"
   21.42  
   21.43 -    assign  "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \
   21.44 -\            <x := a,sigma> -c-> sigma[m/x]"
   21.45 +    assign  "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> 
   21.46 +            <x := a,sigma> -c-> sigma[m/x]"
   21.47  
   21.48 -    semi    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \
   21.49 -\            <c0 ; c1, sigma> -c-> sigma1"
   21.50 +    semi    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> 
   21.51 +            <c0 ; c1, sigma> -c-> sigma1"
   21.52  
   21.53 -    ifc1     "[| b:bexp; c1:com; sigma:loc->nat;   \
   21.54 -\		 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
   21.55 -\             <ifc b then c0 else c1, sigma> -c-> sigma1"
   21.56 +    ifc1     "[| b:bexp; c1:com; sigma:loc->nat;   
   21.57 +		 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> 
   21.58 +             <ifc b then c0 else c1, sigma> -c-> sigma1"
   21.59  
   21.60 -    ifc0     "[| b:bexp; c0:com; sigma:loc->nat;   \
   21.61 -\		 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \
   21.62 -\             <ifc b then c0 else c1, sigma> -c-> sigma1"
   21.63 +    ifc0     "[| b:bexp; c0:com; sigma:loc->nat;   
   21.64 +		 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> 
   21.65 +             <ifc b then c0 else c1, sigma> -c-> sigma1"
   21.66  
   21.67 -    while0   "[| c: com; <b, sigma> -b-> 0 |] ==> \
   21.68 -\             <while b do c,sigma> -c-> sigma "
   21.69 +    while0   "[| c: com; <b, sigma> -b-> 0 |] ==> 
   21.70 +             <while b do c,sigma> -c-> sigma "
   21.71  
   21.72 -    while1   "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \
   21.73 -\                <while b do c, sigma2> -c-> sigma1 |] ==> \
   21.74 -\             <while b do c, sigma> -c-> sigma1 "
   21.75 +    while1   "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; 
   21.76 +                <while b do c, sigma2> -c-> sigma1 |] ==> 
   21.77 +             <while b do c, sigma> -c-> sigma1 "
   21.78  
   21.79    con_defs   "[assign_def]"
   21.80    type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
   21.81 -  type_elims "[make_elim(evala.dom_subset RS subsetD),   \
   21.82 -\	      make_elim(evalb.dom_subset RS subsetD) ]"
   21.83 +  type_elims "[make_elim(evala.dom_subset RS subsetD),   
   21.84 +	      make_elim(evalb.dom_subset RS subsetD) ]"
   21.85  
   21.86  end
    22.1 --- a/src/ZF/IMP/Denotation.thy	Thu Jun 22 12:58:39 1995 +0200
    22.2 +++ b/src/ZF/IMP/Denotation.thy	Thu Jun 22 17:13:05 1995 +0200
    22.3 @@ -31,15 +31,15 @@
    22.4    B_or_def	"B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
    22.5  
    22.6    C_skip_def	"C(skip) == id(loc->nat)"
    22.7 -  C_assign_def	"C(x := a) == {io:(loc->nat)*(loc->nat). \
    22.8 -\			       snd(io) = fst(io)[A(a,fst(io))/x]}"
    22.9 +  C_assign_def	"C(x := a) == {io:(loc->nat)*(loc->nat). 
   22.10 +			       snd(io) = fst(io)[A(a,fst(io))/x]}"
   22.11  
   22.12    C_comp_def	"C(c0 ; c1) == C(c1) O C(c0)"
   22.13 -  C_if_def	"C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un \
   22.14 -\			 	             {io:C(c1). B(b,fst(io))=0}"
   22.15 +  C_if_def	"C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un 
   22.16 +			 	             {io:C(c1). B(b,fst(io))=0}"
   22.17  
   22.18 -  Gamma_def	"Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un \
   22.19 -\			 	     {io : id(loc->nat). B(b,fst(io))=0})"
   22.20 +  Gamma_def	"Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un 
   22.21 +			 	     {io : id(loc->nat). B(b,fst(io))=0})"
   22.22  
   22.23    C_while_def	"C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
   22.24  
    23.1 --- a/src/ZF/Nat.thy	Thu Jun 22 12:58:39 1995 +0200
    23.2 +++ b/src/ZF/Nat.thy	Thu Jun 22 17:13:05 1995 +0200
    23.3 @@ -20,7 +20,7 @@
    23.4  	"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
    23.5  
    23.6      nat_rec_def
    23.7 -	"nat_rec(k,a,b) ==   \
    23.8 -\   	  wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
    23.9 +	"nat_rec(k,a,b) ==   
   23.10 +   	  wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
   23.11  
   23.12  end
    24.1 --- a/src/ZF/Order.thy	Thu Jun 22 12:58:39 1995 +0200
    24.2 +++ b/src/ZF/Order.thy	Thu Jun 22 17:13:05 1995 +0200
    24.3 @@ -25,17 +25,17 @@
    24.4  
    24.5    well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
    24.6  
    24.7 -  mono_map_def "mono_map(A,r,B,s) == \
    24.8 -\                   {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
    24.9 +  mono_map_def "mono_map(A,r,B,s) == 
   24.10 +                   {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
   24.11  
   24.12 -  ord_iso_def  "ord_iso(A,r,B,s) == \
   24.13 -\                   {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
   24.14 +  ord_iso_def  "ord_iso(A,r,B,s) == 
   24.15 +                   {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
   24.16  
   24.17    pred_def     "pred(A,x,r) == {y:A. <y,x>:r}"
   24.18  
   24.19    ord_iso_map_def
   24.20 -     "ord_iso_map(A,r,B,s) == \
   24.21 -\       UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s).   \
   24.22 -\            {<x,y>}"
   24.23 +     "ord_iso_map(A,r,B,s) == 
   24.24 +       UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s).   
   24.25 +            {<x,y>}"
   24.26  
   24.27  end
    25.1 --- a/src/ZF/OrderArith.thy	Thu Jun 22 12:58:39 1995 +0200
    25.2 +++ b/src/ZF/OrderArith.thy	Thu Jun 22 17:13:05 1995 +0200
    25.3 @@ -13,17 +13,17 @@
    25.4  
    25.5  defs
    25.6    (*disjoint sum of two relations; underlies ordinal addition*)
    25.7 -  radd_def "radd(A,r,B,s) == \
    25.8 -\                {z: (A+B) * (A+B).  \
    25.9 -\                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 \
   25.10 -\                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 \
   25.11 -\                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
   25.12 +  radd_def "radd(A,r,B,s) == 
   25.13 +                {z: (A+B) * (A+B).  
   25.14 +                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 
   25.15 +                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 
   25.16 +                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
   25.17  
   25.18    (*lexicographic product of two relations; underlies ordinal multiplication*)
   25.19 -  rmult_def "rmult(A,r,B,s) == \
   25.20 -\                {z: (A*B) * (A*B).  \
   25.21 -\                    EX x' y' x y. z = <<x',y'>, <x,y>> &	 \
   25.22 -\                       (<x',x>: r | (x'=x & <y',y>: s))}"
   25.23 +  rmult_def "rmult(A,r,B,s) == 
   25.24 +                {z: (A*B) * (A*B).  
   25.25 +                    EX x' y' x y. z = <<x',y'>, <x,y>> &	 
   25.26 +                       (<x',x>: r | (x'=x & <y',y>: s))}"
   25.27  
   25.28    (*inverse image of a relation*)
   25.29    rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
    26.1 --- a/src/ZF/Perm.thy	Thu Jun 22 12:58:39 1995 +0200
    26.2 +++ b/src/ZF/Perm.thy	Thu Jun 22 17:13:05 1995 +0200
    26.3 @@ -18,8 +18,8 @@
    26.4  defs
    26.5  
    26.6      (*composition of relations and functions; NOT Suppes's relative product*)
    26.7 -    comp_def	"r O s == {xz : domain(s)*range(r) . \
    26.8 -\                  		EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
    26.9 +    comp_def	"r O s == {xz : domain(s)*range(r) . 
   26.10 +                  		EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
   26.11  
   26.12      (*the identity function for A*)
   26.13      id_def	"id(A) == (lam x:A. x)"
    27.1 --- a/src/ZF/Rel.thy	Thu Jun 22 12:58:39 1995 +0200
    27.2 +++ b/src/ZF/Rel.thy	Thu Jun 22 17:13:05 1995 +0200
    27.3 @@ -25,8 +25,8 @@
    27.4  
    27.5    trans_def    "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
    27.6  
    27.7 -  trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. 	\
    27.8 -\                          <x,y>: r --> <y,z>: r --> <x,z>: r"
    27.9 +  trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. 	
   27.10 +                          <x,y>: r --> <y,z>: r --> <x,z>: r"
   27.11  
   27.12    equiv_def    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
   27.13  
    28.1 --- a/src/ZF/Resid/Confluence.thy	Thu Jun 22 12:58:39 1995 +0200
    28.2 +++ b/src/ZF/Resid/Confluence.thy	Thu Jun 22 17:13:05 1995 +0200
    28.3 @@ -12,10 +12,10 @@
    28.4    strip		:: "o"
    28.5  
    28.6  defs
    28.7 -  confluence_def "confluence(R) ==   \
    28.8 -\		  ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->   \
    28.9 -\		                         (EX u.<y,u>:R & <z,u>:R))"
   28.10 -  strip_def      "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->   \
   28.11 -\		                         (EX u.(y =1=> u) & (z===>u)))" 
   28.12 +  confluence_def "confluence(R) ==   
   28.13 +		  ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->   
   28.14 +		                         (EX u.<y,u>:R & <z,u>:R))"
   28.15 +  strip_def      "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->   
   28.16 +		                         (EX u.(y =1=> u) & (z===>u)))" 
   28.17  end
   28.18  
    29.1 --- a/src/ZF/Resid/Redex.thy	Thu Jun 22 12:58:39 1995 +0200
    29.2 +++ b/src/ZF/Resid/Redex.thy	Thu Jun 22 17:13:05 1995 +0200
    29.3 @@ -21,8 +21,8 @@
    29.4   
    29.5  defs
    29.6    redex_rec_def
    29.7 -   "redex_rec(p,b,c,d) == \
    29.8 -\   Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),   \
    29.9 -\                             %n x y.d(n, x, y, g`x, g`y), p))"
   29.10 +   "redex_rec(p,b,c,d) == 
   29.11 +   Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),   
   29.12 +                             %n x y.d(n, x, y, g`x, g`y), p))"
   29.13  end
   29.14  
    30.1 --- a/src/ZF/Resid/Reduction.thy	Thu Jun 22 12:58:39 1995 +0200
    30.2 +++ b/src/ZF/Resid/Reduction.thy	Thu Jun 22 17:13:05 1995 +0200
    30.3 @@ -23,10 +23,10 @@
    30.4    intrs
    30.5      beta	"[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
    30.6      rfun  	"[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
    30.7 -    apl_l	"[|m2:lambda; m1 -1-> n1|] ==>   \
    30.8 -\		 	          Apl(m1,m2) -1-> Apl(n1,m2)"
    30.9 -    apl_r	"[|m1:lambda; m2 -1-> n2|] ==>   \
   30.10 -\		 	          Apl(m1,m2) -1-> Apl(m1,n2)"
   30.11 +    apl_l	"[|m2:lambda; m1 -1-> n1|] ==>   
   30.12 +		 	          Apl(m1,m2) -1-> Apl(n1,m2)"
   30.13 +    apl_r	"[|m1:lambda; m2 -1-> n2|] ==>   
   30.14 +		 	          Apl(m1,m2) -1-> Apl(m1,n2)"
   30.15    type_intrs	"red_typechecks"
   30.16  
   30.17  inductive
   30.18 @@ -40,12 +40,12 @@
   30.19  inductive
   30.20    domains       "Spar_red1" <= "lambda*lambda"
   30.21    intrs
   30.22 -    beta	"[|m =1=> m';   \
   30.23 -\		 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
   30.24 +    beta	"[|m =1=> m';   
   30.25 +		 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
   30.26      rvar	"n:nat==> Var(n) =1=> Var(n)"
   30.27      rfun	"[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
   30.28 -    rapl	"[|m =1=> m';   \
   30.29 -\		 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
   30.30 +    rapl	"[|m =1=> m';   
   30.31 +		 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
   30.32    type_intrs	"red_typechecks"
   30.33  
   30.34    inductive
    31.1 --- a/src/ZF/Resid/Residuals.thy	Thu Jun 22 12:58:39 1995 +0200
    31.2 +++ b/src/ZF/Resid/Residuals.thy	Thu Jun 22 17:13:05 1995 +0200
    31.3 @@ -20,14 +20,14 @@
    31.4    domains       "Sres" <= "redexes*redexes*redexes"
    31.5    intrs
    31.6      Res_Var	"n:nat ==> residuals(Var(n),Var(n),Var(n))"
    31.7 -    Res_Fun	"[|residuals(u,v,w)|]==>   \
    31.8 -\		     residuals(Fun(u),Fun(v),Fun(w))"
    31.9 -    Res_App	"[|residuals(u1,v1,w1);   \
   31.10 -\		   residuals(u2,v2,w2); b:bool|]==>   \
   31.11 -\		 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
   31.12 -    Res_redex	"[|residuals(u1,v1,w1);   \
   31.13 -\		   residuals(u2,v2,w2); b:bool|]==>   \
   31.14 -\		 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
   31.15 +    Res_Fun	"[|residuals(u,v,w)|]==>   
   31.16 +		     residuals(Fun(u),Fun(v),Fun(w))"
   31.17 +    Res_App	"[|residuals(u1,v1,w1);   
   31.18 +		   residuals(u2,v2,w2); b:bool|]==>   
   31.19 +		 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
   31.20 +    Res_redex	"[|residuals(u1,v1,w1);   
   31.21 +		   residuals(u2,v2,w2); b:bool|]==>   
   31.22 +		 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
   31.23    type_intrs	"[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
   31.24  
   31.25  rules
    32.1 --- a/src/ZF/Resid/SubUnion.thy	Thu Jun 22 12:58:39 1995 +0200
    32.2 +++ b/src/ZF/Resid/SubUnion.thy	Thu Jun 22 17:13:05 1995 +0200
    32.3 @@ -23,10 +23,10 @@
    32.4    intrs
    32.5      Sub_Var	"n:nat ==> Var(n)<== Var(n)"
    32.6      Sub_Fun	"[|u<== v|]==> Fun(u)<== Fun(v)"
    32.7 -    Sub_App1	"[|u1<== v1; u2<== v2; b:bool|]==>   \
    32.8 -\		     App(0,u1,u2)<== App(b,v1,v2)"
    32.9 -    Sub_App2	"[|u1<== v1; u2<== v2|]==>   \
   32.10 -\		     App(1,u1,u2)<== App(1,v1,v2)"
   32.11 +    Sub_App1	"[|u1<== v1; u2<== v2; b:bool|]==>   
   32.12 +		     App(0,u1,u2)<== App(b,v1,v2)"
   32.13 +    Sub_App2	"[|u1<== v1; u2<== v2|]==>   
   32.14 +		     App(1,u1,u2)<== App(1,v1,v2)"
   32.15    type_intrs	"redexes.intrs@bool_typechecks"
   32.16  
   32.17  inductive
   32.18 @@ -34,8 +34,8 @@
   32.19    intrs
   32.20      Comp_Var	"n:nat ==> Var(n) ~ Var(n)"
   32.21      Comp_Fun	"[|u ~ v|]==> Fun(u) ~ Fun(v)"
   32.22 -    Comp_App	"[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>   \
   32.23 -\		     App(b1,u1,u2) ~ App(b2,v1,v2)"
   32.24 +    Comp_App	"[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>   
   32.25 +		     App(b1,u1,u2) ~ App(b2,v1,v2)"
   32.26    type_intrs	"redexes.intrs@bool_typechecks"
   32.27  
   32.28  inductive
   32.29 @@ -43,17 +43,17 @@
   32.30    intrs
   32.31      Reg_Var	"n:nat ==> regular(Var(n))"
   32.32      Reg_Fun	"[|regular(u)|]==> regular(Fun(u))"
   32.33 -    Reg_App1	"[|regular(Fun(u)); regular(v) \
   32.34 -\		     |]==>regular(App(1,Fun(u),v))"
   32.35 -    Reg_App2	"[|regular(u); regular(v) \
   32.36 -\		     |]==>regular(App(0,u,v))"
   32.37 +    Reg_App1	"[|regular(Fun(u)); regular(v) 
   32.38 +		     |]==>regular(App(1,Fun(u),v))"
   32.39 +    Reg_App2	"[|regular(u); regular(v) 
   32.40 +		     |]==>regular(App(0,u,v))"
   32.41    type_intrs	"redexes.intrs@bool_typechecks"
   32.42  
   32.43  defs
   32.44 -  union_def  "u un v == redex_rec(u,   \
   32.45 -\	 %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),   \
   32.46 -\      %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),   \
   32.47 -\%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,   \
   32.48 -\	                               %c z u. App(b or c, m`z, p`u), t))`v"
   32.49 +  union_def  "u un v == redex_rec(u,   
   32.50 +	 %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),   
   32.51 +      %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),   
   32.52 +%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,   
   32.53 +	                               %c z u. App(b or c, m`z, p`u), t))`v"
   32.54  end
   32.55  
    33.1 --- a/src/ZF/Resid/Substitution.thy	Thu Jun 22 12:58:39 1995 +0200
    33.2 +++ b/src/ZF/Resid/Substitution.thy	Thu Jun 22 17:13:05 1995 +0200
    33.3 @@ -17,10 +17,10 @@
    33.4    "u/v" == "subst_rec(u,v,0)"
    33.5    
    33.6  defs
    33.7 -  lift_rec_def	"lift_rec(r,kg) ==   \
    33.8 -\		     redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), \
    33.9 -\		                 %x m.(lam k:nat.Fun(m`(succ(k)))),   \
   33.10 -\		                 %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
   33.11 +  lift_rec_def	"lift_rec(r,kg) ==   
   33.12 +		     redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), 
   33.13 +		                 %x m.(lam k:nat.Fun(m`(succ(k)))),   
   33.14 +		                 %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
   33.15  
   33.16    
   33.17  (* subst_rec(u,Var(i),k)     = if k<i then Var(i-1)
   33.18 @@ -30,15 +30,15 @@
   33.19     subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))
   33.20  
   33.21  *)
   33.22 -  subst_rec_def	"subst_rec(u,t,kg) ==   \
   33.23 -\		     redex_rec(t,   \
   33.24 -\		       %i.(lam r:redexes.lam k:nat.   \
   33.25 -\		              if(k<i,Var(i#-1),   \
   33.26 -\		                if(k=i,r,Var(i)))),   \
   33.27 -\		       %x m.(lam r:redexes.lam k:nat.   \
   33.28 -\                             Fun(m`(lift(r))`(succ(k)))),   \
   33.29 -\		       %b x y m p.lam r:redexes.lam k:nat.   \
   33.30 -\		              App(b,m`r`k,p`r`k))`u`kg"
   33.31 +  subst_rec_def	"subst_rec(u,t,kg) ==   
   33.32 +		     redex_rec(t,   
   33.33 +		       %i.(lam r:redexes.lam k:nat.   
   33.34 +		              if(k<i,Var(i#-1),   
   33.35 +		                if(k=i,r,Var(i)))),   
   33.36 +		       %x m.(lam r:redexes.lam k:nat.   
   33.37 +                             Fun(m`(lift(r))`(succ(k)))),   
   33.38 +		       %b x y m p.lam r:redexes.lam k:nat.   
   33.39 +		              App(b,m`r`k,p`r`k))`u`kg"
   33.40  
   33.41  
   33.42  end
    34.1 --- a/src/ZF/Resid/Terms.thy	Thu Jun 22 12:58:39 1995 +0200
    34.2 +++ b/src/ZF/Resid/Terms.thy	Thu Jun 22 17:13:05 1995 +0200
    34.3 @@ -24,9 +24,9 @@
    34.4    type_intrs	"redexes.intrs@bool_typechecks"
    34.5  
    34.6  defs
    34.7 -  unmark_def	"unmark(u) == redex_rec(u,%i.Var(i),   \
    34.8 -\		                          %x m.Fun(m),   \
    34.9 -\		                          %b x y m p.Apl(m,p))"
   34.10 +  unmark_def	"unmark(u) == redex_rec(u,%i.Var(i),   
   34.11 +		                          %x m.Fun(m),   
   34.12 +		                          %b x y m p.Apl(m,p))"
   34.13  end
   34.14  
   34.15  
    35.1 --- a/src/ZF/Univ.thy	Thu Jun 22 12:58:39 1995 +0200
    35.2 +++ b/src/ZF/Univ.thy	Thu Jun 22 17:13:05 1995 +0200
    35.3 @@ -25,8 +25,8 @@
    35.4      Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
    35.5  
    35.6      Vrec_def
    35.7 -   	"Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      \
    35.8 -\                             H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
    35.9 +   	"Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
   35.10 +                             H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
   35.11  
   35.12      univ_def    "univ(A) == Vfrom(A,nat)"
   35.13  
    36.1 --- a/src/ZF/WF.thy	Thu Jun 22 12:58:39 1995 +0200
    36.2 +++ b/src/ZF/WF.thy	Thu Jun 22 17:13:05 1995 +0200
    36.3 @@ -23,8 +23,8 @@
    36.4    (*r is well-founded relation over A*)
    36.5    wf_on_def      "wf_on(A,r) == wf(r Int A*A)"
    36.6  
    36.7 -  is_recfun_def  "is_recfun(r,a,H,f) == \
    36.8 -\   			(f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
    36.9 +  is_recfun_def  "is_recfun(r,a,H,f) == 
   36.10 +   			(f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
   36.11  
   36.12    the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))"
   36.13  
    37.1 --- a/src/ZF/ZF.thy	Thu Jun 22 12:58:39 1995 +0200
    37.2 +++ b/src/ZF/ZF.thy	Thu Jun 22 17:13:05 1995 +0200
    37.3 @@ -159,8 +159,8 @@
    37.4    foundation    "A=0 | (EX x:A. ALL y:x. y~:A)"
    37.5  
    37.6    (*Schema axiom since predicate P is a higher-order variable*)
    37.7 -  replacement   "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \
    37.8 -                \        b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
    37.9 +  replacement   "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> 
   37.10 +                         b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
   37.11  
   37.12  defs
   37.13  
   37.14 @@ -214,8 +214,8 @@
   37.15    domain_def    "domain(r) == {x. w:r, EX y. w=<x,y>}"
   37.16    range_def     "range(r) == domain(converse(r))"
   37.17    field_def     "field(r) == domain(r) Un range(r)"
   37.18 -  function_def	"function(r) == ALL x y. <x,y>:r -->   \
   37.19 -\		                (ALL y'. <x,y'>:r --> y=y')"
   37.20 +  function_def	"function(r) == ALL x y. <x,y>:r -->   
   37.21 +		                (ALL y'. <x,y'>:r --> y=y')"
   37.22    image_def     "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
   37.23    vimage_def    "r -`` A == converse(r)``A"
   37.24  
    38.1 --- a/src/ZF/Zorn.thy	Thu Jun 22 12:58:39 1995 +0200
    38.2 +++ b/src/ZF/Zorn.thy	Thu Jun 22 17:13:05 1995 +0200
    38.3 @@ -39,8 +39,8 @@
    38.4  inductive
    38.5    domains       "TFin(S,next)" <= "Pow(S)"
    38.6    intrs
    38.7 -    nextI	"[| x : TFin(S,next);  next: increasing(S) \
    38.8 -\                |] ==> next`x : TFin(S,next)"
    38.9 +    nextI	"[| x : TFin(S,next);  next: increasing(S) 
   38.10 +                |] ==> next`x : TFin(S,next)"
   38.11  
   38.12      Pow_UnionI	"Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
   38.13  
    39.1 --- a/src/ZF/ex/Bin.thy	Thu Jun 22 12:58:39 1995 +0200
    39.2 +++ b/src/ZF/ex/Bin.thy	Thu Jun 22 17:13:05 1995 +0200
    39.3 @@ -44,8 +44,8 @@
    39.4  defs
    39.5  
    39.6    bin_rec_def
    39.7 -      "bin_rec(z,a,b,h) == \
    39.8 -\      Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
    39.9 +      "bin_rec(z,a,b,h) == 
   39.10 +      Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
   39.11  
   39.12    integ_of_bin_def
   39.13        "integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
   39.14 @@ -54,39 +54,39 @@
   39.15  
   39.16    (*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
   39.17    norm_Bcons_def
   39.18 -      "norm_Bcons(w,b) ==   \
   39.19 -\       bin_case(cond(b,Bcons(w,b),w), cond(b,w,Bcons(w,b)),   \
   39.20 -\                %w' x'. Bcons(w,b), w)"
   39.21 +      "norm_Bcons(w,b) ==   
   39.22 +       bin_case(cond(b,Bcons(w,b),w), cond(b,w,Bcons(w,b)),   
   39.23 +                %w' x'. Bcons(w,b), w)"
   39.24  
   39.25    bin_succ_def
   39.26 -      "bin_succ(w0) ==   \
   39.27 -\       bin_rec(w0, Bcons(Plus,1), Plus,   \
   39.28 -\               %w x r. cond(x, Bcons(r,0), norm_Bcons(w,1)))"
   39.29 +      "bin_succ(w0) ==   
   39.30 +       bin_rec(w0, Bcons(Plus,1), Plus,   
   39.31 +               %w x r. cond(x, Bcons(r,0), norm_Bcons(w,1)))"
   39.32  
   39.33    bin_pred_def
   39.34 -      "bin_pred(w0) == \
   39.35 -\       bin_rec(w0, Minus, Bcons(Minus,0),   \
   39.36 -\               %w x r. cond(x, norm_Bcons(w,0), Bcons(r,1)))"
   39.37 +      "bin_pred(w0) == 
   39.38 +       bin_rec(w0, Minus, Bcons(Minus,0),   
   39.39 +               %w x r. cond(x, norm_Bcons(w,0), Bcons(r,1)))"
   39.40  
   39.41    bin_minus_def
   39.42 -      "bin_minus(w0) == \
   39.43 -\       bin_rec(w0, Plus, Bcons(Plus,1),   \
   39.44 -\               %w x r. cond(x, bin_pred(Bcons(r,0)), Bcons(r,0)))"
   39.45 +      "bin_minus(w0) == 
   39.46 +       bin_rec(w0, Plus, Bcons(Plus,1),   
   39.47 +               %w x r. cond(x, bin_pred(Bcons(r,0)), Bcons(r,0)))"
   39.48  
   39.49    bin_add_def
   39.50 -      "bin_add(v0,w0) ==                        \
   39.51 -\       bin_rec(v0,                             \
   39.52 -\         lam w:bin. w,                 \
   39.53 -\         lam w:bin. bin_pred(w),       \
   39.54 -\         %v x r. lam w1:bin.           \
   39.55 -\                  bin_rec(w1, Bcons(v,x), bin_pred(Bcons(v,x)),    \
   39.56 -\                    %w y s. norm_Bcons(r`cond(x and y, bin_succ(w), w), \
   39.57 -\                                          x xor y)))    ` w0"
   39.58 +      "bin_add(v0,w0) ==                        
   39.59 +       bin_rec(v0,                             
   39.60 +         lam w:bin. w,                 
   39.61 +         lam w:bin. bin_pred(w),       
   39.62 +         %v x r. lam w1:bin.           
   39.63 +                  bin_rec(w1, Bcons(v,x), bin_pred(Bcons(v,x)),    
   39.64 +                    %w y s. norm_Bcons(r`cond(x and y, bin_succ(w), w), 
   39.65 +                                          x xor y)))    ` w0"
   39.66  
   39.67    bin_mult_def
   39.68 -      "bin_mult(v0,w) ==                        \
   39.69 -\       bin_rec(v0, Plus, bin_minus(w),         \
   39.70 -\         %v x r. cond(x, bin_add(norm_Bcons(r,0),w), norm_Bcons(r,0)))"
   39.71 +      "bin_mult(v0,w) ==                        
   39.72 +       bin_rec(v0, Plus, bin_minus(w),         
   39.73 +         %v x r. cond(x, bin_add(norm_Bcons(r,0),w), norm_Bcons(r,0)))"
   39.74  end
   39.75  
   39.76  
    40.1 --- a/src/ZF/ex/Brouwer.thy	Thu Jun 22 12:58:39 1995 +0200
    40.2 +++ b/src/ZF/ex/Brouwer.thy	Thu Jun 22 17:13:05 1995 +0200
    40.3 @@ -22,8 +22,8 @@
    40.4  datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
    40.5    "Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
    40.6    monos	      "[Pi_mono]"
    40.7 -  type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   \
    40.8 -\	       @ inf_datatype_intrs"
    40.9 +  type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   
   40.10 +	       @ inf_datatype_intrs"
   40.11  
   40.12  
   40.13  end
    41.1 --- a/src/ZF/ex/Comb.thy	Thu Jun 22 12:58:39 1995 +0200
    41.2 +++ b/src/ZF/ex/Comb.thy	Thu Jun 22 17:13:05 1995 +0200
    41.3 @@ -73,9 +73,9 @@
    41.4  
    41.5  defs
    41.6  
    41.7 -  diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
    41.8 -\                            (ALL y'. <x,y'>:r --> \
    41.9 -\                                 (EX z. <y,z>:r & <y',z> : r))"
   41.10 +  diamond_def "diamond(r) == ALL x y. <x,y>:r --> 
   41.11 +                            (ALL y'. <x,y'>:r --> 
   41.12 +                                 (EX z. <y,z>:r & <y',z> : r))"
   41.13  
   41.14    I_def       "I == S#K#K"
   41.15  
    42.1 --- a/src/ZF/ex/Integ.thy	Thu Jun 22 12:58:39 1995 +0200
    42.2 +++ b/src/ZF/ex/Integ.thy	Thu Jun 22 17:13:05 1995 +0200
    42.3 @@ -23,8 +23,8 @@
    42.4  defs
    42.5  
    42.6      intrel_def
    42.7 -     "intrel == {p:(nat*nat)*(nat*nat). 		\
    42.8 -\        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    42.9 +     "intrel == {p:(nat*nat)*(nat*nat). 		
   42.10 +        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
   42.11  
   42.12      integ_def   "integ == (nat*nat)/intrel"
   42.13      
   42.14 @@ -42,17 +42,17 @@
   42.15        Perhaps a "curried" or even polymorphic congruent predicate would be
   42.16        better.*)
   42.17      zadd_def
   42.18 -     "Z1 $+ Z2 == \
   42.19 -\       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 \
   42.20 -\                           in intrel``{<x1#+x2, y1#+y2>}"
   42.21 +     "Z1 $+ Z2 == 
   42.22 +       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
   42.23 +                           in intrel``{<x1#+x2, y1#+y2>}"
   42.24      
   42.25      zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
   42.26      zless_def	"Z1 $< Z2 == znegative(Z1 $- Z2)"
   42.27      
   42.28      (*This illustrates the primitive form of definitions (no patterns)*)
   42.29      zmult_def
   42.30 -     "Z1 $* Z2 == \
   42.31 -\       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        \
   42.32 -\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
   42.33 +     "Z1 $* Z2 == 
   42.34 +       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
   42.35 +                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
   42.36      
   42.37   end
    43.1 --- a/src/ZF/ex/LList.thy	Thu Jun 22 12:58:39 1995 +0200
    43.2 +++ b/src/ZF/ex/LList.thy	Thu Jun 22 17:13:05 1995 +0200
    43.3 @@ -49,8 +49,8 @@
    43.4  rules
    43.5    flip_LNil   "flip(LNil) = LNil"
    43.6  
    43.7 -  flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
    43.8 -\              flip(LCons(x,l)) = LCons(not(x), flip(l))"
    43.9 +  flip_LCons  "[| x:bool; l: llist(bool) |] ==> 
   43.10 +              flip(LCons(x,l)) = LCons(not(x), flip(l))"
   43.11  
   43.12  end
   43.13  
    44.1 --- a/src/ZF/ex/Primrec.thy	Thu Jun 22 12:58:39 1995 +0200
    44.2 +++ b/src/ZF/ex/Primrec.thy	Thu Jun 22 17:13:05 1995 +0200
    44.3 @@ -39,12 +39,12 @@
    44.4    COMP_def  "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)"
    44.5  
    44.6    (*Note that g is applied first to PREC(f,g)`y and then to y!*)
    44.7 -  PREC_def  "PREC(f,g) == \
    44.8 -\            lam l:list(nat). list_case(0, \
    44.9 -\                      %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
   44.10 +  PREC_def  "PREC(f,g) == 
   44.11 +            lam l:list(nat). list_case(0, 
   44.12 +                      %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
   44.13    
   44.14 -  ACK_def   "ACK(i) == rec(i, SC, \
   44.15 -\                      %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
   44.16 +  ACK_def   "ACK(i) == rec(i, SC, 
   44.17 +                      %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
   44.18  
   44.19  
   44.20  inductive
   44.21 @@ -57,8 +57,8 @@
   44.22      PREC     "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
   44.23    monos      "[list_mono]"
   44.24    con_defs   "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
   44.25 -  type_intrs "nat_typechecks @ list.intrs @   		        \
   44.26 -\	      [lam_type, list_case_type, drop_type, map_type,   \
   44.27 -\	      apply_type, rec_type]"
   44.28 +  type_intrs "nat_typechecks @ list.intrs @   		        
   44.29 +	      [lam_type, list_case_type, drop_type, map_type,   
   44.30 +	      apply_type, rec_type]"
   44.31  
   44.32  end
    45.1 --- a/src/ZF/ex/PropLog.thy	Thu Jun 22 12:58:39 1995 +0200
    45.2 +++ b/src/ZF/ex/PropLog.thy	Thu Jun 22 17:13:05 1995 +0200
    45.3 @@ -47,13 +47,13 @@
    45.4  defs
    45.5  
    45.6    prop_rec_def
    45.7 -   "prop_rec(p,b,c,h) == \
    45.8 -\   Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
    45.9 +   "prop_rec(p,b,c,h) == 
   45.10 +   Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
   45.11  
   45.12    (** Semantics of propositional logic **)
   45.13    is_true_def
   45.14 -   "is_true(p,t) == prop_rec(p, 0,  %v. if(v:t, 1, 0), \
   45.15 -\                               %p q tp tq. if(tp=1,tq,1))         =  1"
   45.16 +   "is_true(p,t) == prop_rec(p, 0,  %v. if(v:t, 1, 0), 
   45.17 +                               %p q tp tq. if(tp=1,tq,1))         =  1"
   45.18  
   45.19    (*Logical consequence: for every valuation, if all elements of H are true
   45.20       then so is p*)
   45.21 @@ -61,7 +61,7 @@
   45.22  
   45.23    (** A finite set of hypotheses from t and the Vars in p **)
   45.24    hyps_def
   45.25 -   "hyps(p,t) == prop_rec(p, 0,  %v. {if(v:t, #v, #v=>Fls)}, \
   45.26 -\                            %p q Hp Hq. Hp Un Hq)"
   45.27 +   "hyps(p,t) == prop_rec(p, 0,  %v. {if(v:t, #v, #v=>Fls)}, 
   45.28 +                            %p q Hp Hq. Hp Un Hq)"
   45.29  
   45.30  end
    46.1 --- a/src/ZF/ex/Ramsey.thy	Thu Jun 22 12:58:39 1995 +0200
    46.2 +++ b/src/ZF/ex/Ramsey.thy	Thu Jun 22 17:13:05 1995 +0200
    46.3 @@ -39,8 +39,8 @@
    46.4      "Atleast(n,S) == (EX f. f: inj(n,S))"
    46.5  
    46.6    Ramsey_def
    46.7 -    "Ramsey(n,i,j) == ALL V E. Symmetric(E) & Atleast(n,V) -->  \
    46.8 -\         (EX C. Clique(C,V,E) & Atleast(i,C)) |       \
    46.9 -\         (EX I. Indept(I,V,E) & Atleast(j,I))"
   46.10 +    "Ramsey(n,i,j) == ALL V E. Symmetric(E) & Atleast(n,V) -->  
   46.11 +         (EX C. Clique(C,V,E) & Atleast(i,C)) |       
   46.12 +         (EX I. Indept(I,V,E) & Atleast(j,I))"
   46.13  
   46.14  end
    47.1 --- a/src/ZF/ex/Rmap.thy	Thu Jun 22 12:58:39 1995 +0200
    47.2 +++ b/src/ZF/ex/Rmap.thy	Thu Jun 22 17:13:05 1995 +0200
    47.3 @@ -16,8 +16,8 @@
    47.4    intrs
    47.5      NilI  "<Nil,Nil> : rmap(r)"
    47.6  
    47.7 -    ConsI "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> \
    47.8 -\          <Cons(x,xs), Cons(y,ys)> : rmap(r)"
    47.9 +    ConsI "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> 
   47.10 +          <Cons(x,xs), Cons(y,ys)> : rmap(r)"
   47.11  
   47.12    type_intrs "[domainI,rangeI] @ list.intrs"
   47.13  
    48.1 --- a/src/ZF/ex/TF.thy	Thu Jun 22 12:58:39 1995 +0200
    48.2 +++ b/src/ZF/ex/TF.thy	Thu Jun 22 17:13:05 1995 +0200
    48.3 @@ -24,21 +24,21 @@
    48.4  
    48.5  defs
    48.6    TF_rec_def
    48.7 -    "TF_rec(z,b,c,d) == Vrec(z,  			\
    48.8 -\      %z r. tree_forest_case(%x f. b(x, f, r`f), 	\
    48.9 -\                             c, 			\
   48.10 -\		              %t f. d(t, f, r`t, r`f), z))"
   48.11 +    "TF_rec(z,b,c,d) == Vrec(z,  			
   48.12 +      %z r. tree_forest_case(%x f. b(x, f, r`f), 	
   48.13 +                             c, 			
   48.14 +		              %t f. d(t, f, r`t, r`f), z))"
   48.15  
   48.16    list_of_TF_def
   48.17 -    "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], \
   48.18 -\		             %t f r1 r2. Cons(t, r2))"
   48.19 +    "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], 
   48.20 +		             %t f r1 r2. Cons(t, r2))"
   48.21  
   48.22    TF_of_list_def
   48.23      "TF_of_list(f) == list_rec(f, Fnil,  %t f r. Fcons(t,r))"
   48.24  
   48.25    TF_map_def
   48.26 -    "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, \
   48.27 -\                           %t f r1 r2. Fcons(r1,r2))"
   48.28 +    "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, 
   48.29 +                           %t f r1 r2. Fcons(r1,r2))"
   48.30  
   48.31    TF_size_def
   48.32      "TF_size(z) == TF_rec(z, %x f r.succ(r), 0, %t f r1 r2. r1#+r2)"
    49.1 --- a/src/ZF/ex/Term.thy	Thu Jun 22 12:58:39 1995 +0200
    49.2 +++ b/src/ZF/ex/Term.thy	Thu Jun 22 17:13:05 1995 +0200
    49.3 @@ -28,8 +28,8 @@
    49.4  
    49.5  defs
    49.6    term_rec_def
    49.7 -   "term_rec(t,d) == \
    49.8 -\   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
    49.9 +   "term_rec(t,d) == 
   49.10 +   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
   49.11  
   49.12    term_map_def	"term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
   49.13