expanded tabs
authorclasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 14782b8c2a7547ab
parent 1477 4c51ab632cda
child 1479 21eb5e156d91
expanded tabs
src/ZF/AC.thy
src/ZF/AC/AC16_WO4.thy
src/ZF/AC/AC18_AC19.thy
src/ZF/AC/AC_Equiv.thy
src/ZF/AC/DC.thy
src/ZF/AC/HH.thy
src/ZF/AC/Hartog.thy
src/ZF/AC/OrdQuant.thy
src/ZF/AC/Transrec2.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/AC/first.thy
src/ZF/AC/recfunAC16.thy
src/ZF/Arith.thy
src/ZF/Bool.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.thy
src/ZF/Coind/BCR.thy
src/ZF/Coind/Dynamic.thy
src/ZF/Coind/ECR.thy
src/ZF/Coind/Language.thy
src/ZF/Coind/Map.thy
src/ZF/Coind/Static.thy
src/ZF/Coind/Types.thy
src/ZF/Coind/Values.thy
src/ZF/Epsilon.thy
src/ZF/EquivClass.thy
src/ZF/Finite.thy
src/ZF/Fixedpt.thy
src/ZF/IMP/Com.thy
src/ZF/IMP/Denotation.thy
src/ZF/IMP/Equiv.thy
src/ZF/Let.thy
src/ZF/List.thy
src/ZF/Nat.thy
src/ZF/Order.thy
src/ZF/OrderArith.thy
src/ZF/OrderType.thy
src/ZF/Ordinal.thy
src/ZF/Perm.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Rel.thy
src/ZF/Resid/Confluence.thy
src/ZF/Resid/Conversion.thy
src/ZF/Resid/Cube.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/Sum.thy
src/ZF/Trancl.thy
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/ZF.thy
src/ZF/Zorn.thy
src/ZF/ex/Acc.thy
src/ZF/ex/BT.thy
src/ZF/ex/Brouwer.thy
src/ZF/ex/CoUnit.thy
src/ZF/ex/Comb.thy
src/ZF/ex/Data.thy
src/ZF/ex/Enum.thy
src/ZF/ex/Integ.thy
src/ZF/ex/LList.thy
src/ZF/ex/Limit.thy
src/ZF/ex/ListN.thy
src/ZF/ex/Ntree.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
src/ZF/ex/twos_compl.thy
     1.1 --- a/src/ZF/AC.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/AC.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/AC.thy
     1.5 +(*  Title:      ZF/AC.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1994  University of Cambridge
    1.10  
    1.11  The Axiom of Choice
    1.12 @@ -10,5 +10,5 @@
    1.13  
    1.14  AC = ZF + "func" +
    1.15  rules
    1.16 -  AC	"[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
    1.17 +  AC    "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
    1.18  end
     2.1 --- a/src/ZF/AC/AC16_WO4.thy	Mon Feb 05 21:33:14 1996 +0100
     2.2 +++ b/src/ZF/AC/AC16_WO4.thy	Tue Feb 06 12:27:17 1996 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4 -(*  Title: 	ZF/AC/AC16_WO4.thy
     2.5 +(*  Title:      ZF/AC/AC16_WO4.thy
     2.6      ID:         $Id$
     2.7 -    Author: 	Krzysztof Grabczewski
     2.8 +    Author:     Krzysztof Grabczewski
     2.9  *)
    2.10  
    2.11  AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux +
    2.12 @@ -24,6 +24,6 @@
    2.13    LL_def  "LL(t_n, k, y) == {v Int y. v:MM(t_n, k, y)}"
    2.14  
    2.15    GG_def  "GG(t_n, k, y) == lam v:LL(t_n, k, y). 
    2.16 -	                    (THE w. w:MM(t_n, k, y) & v <= w) - v"
    2.17 +                            (THE w. w:MM(t_n, k, y) & v <= w) - v"
    2.18  
    2.19  end
     3.1 --- a/src/ZF/AC/AC18_AC19.thy	Mon Feb 05 21:33:14 1996 +0100
     3.2 +++ b/src/ZF/AC/AC18_AC19.thy	Tue Feb 06 12:27:17 1996 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4 -(*  Title: 	ZF/AC/AC18_AC19.thy
     3.5 +(*  Title:      ZF/AC/AC18_AC19.thy
     3.6      ID:         $Id$
     3.7 -    Author: 	Krzysztof Grabczewski
     3.8 +    Author:     Krzysztof Grabczewski
     3.9  
    3.10  Additional definition used in the proof AC19 ==> AC1 which is a part
    3.11  of the chain AC1 ==> AC18 ==> AC19 ==> AC1
     4.1 --- a/src/ZF/AC/AC_Equiv.thy	Mon Feb 05 21:33:14 1996 +0100
     4.2 +++ b/src/ZF/AC/AC_Equiv.thy	Tue Feb 06 12:27:17 1996 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4 -(*  Title: 	ZF/AC/AC_Equiv.thy
     4.5 +(*  Title:      ZF/AC/AC_Equiv.thy
     4.6      ID:         $Id$
     4.7 -    Author: 	Krzysztof Grabczewski
     4.8 +    Author:     Krzysztof Grabczewski
     4.9  
    4.10  Axioms AC1 -- AC19 come from "Equivalents of the Axiom of Choice, II"
    4.11  by H. Rubin and J.E. Rubin, 1985.
    4.12 @@ -42,18 +42,18 @@
    4.13    WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
    4.14  
    4.15    WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &   
    4.16 -	             (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
    4.17 +                     (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
    4.18  
    4.19    WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
    4.20  
    4.21    WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a   
    4.22 -	            & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
    4.23 +                    & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
    4.24  
    4.25    WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->   
    4.26 -	            well_ord(A,converse(R)))"
    4.27 +                    well_ord(A,converse(R)))"
    4.28  
    4.29    WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->  
    4.30 -	            (EX R. well_ord(A,R))"
    4.31 +                    (EX R. well_ord(A,R))"
    4.32  
    4.33  (* Axioms of Choice *)  
    4.34  
    4.35 @@ -62,64 +62,64 @@
    4.36    AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
    4.37  
    4.38    AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)   
    4.39 -	            --> (EX C. ALL B:A. EX y. B Int C = {y})"
    4.40 +                    --> (EX C. ALL B:A. EX y. B Int C = {y})"
    4.41  
    4.42    AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
    4.43  
    4.44    AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
    4.45  
    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 +                    ALL x:domain(g). f`(g`x) = x"
    4.49  
    4.50    AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
    4.51  
    4.52    AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)   
    4.53 -	            --> (PROD B:A. B)~=0"
    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 +                    --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
    4.59  
    4.60    AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->   
    4.61 -	            (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
    4.62 +                    (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
    4.63  
    4.64    AC10_def "AC10(n) ==  ALL A. (ALL B:A. ~Finite(B)) -->   
    4.65 -	            (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
    4.66 -	            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=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  
    4.70    AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
    4.71  
    4.72    AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->   
    4.73 -	    (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
    4.74 -	    sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
    4.75 +            (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
    4.76 +            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
    4.77  
    4.78    AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &   
    4.79 -	                                  f`B <= B & f`B lepoll m)"
    4.80 +                                          f`B <= B & f`B lepoll m)"
    4.81  
    4.82    AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
    4.83  
    4.84    AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.   
    4.85 -	                              f`B~=0 & f`B <= B & f`B lepoll m))"
    4.86 +                                      f`B~=0 & f`B <= B & f`B lepoll m))"
    4.87  
    4.88    AC16_def "AC16(n, k)  == ALL A. ~Finite(A) -->   
    4.89 -	    (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   
    4.90 -	    (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
    4.91 +            (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   
    4.92 +            (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
    4.93  
    4.94    AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.   
    4.95 -	            EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
    4.96 +                    EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
    4.97  
    4.98    AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->   
    4.99                   ((INT a:A. UN b:B(a). X(a,b)) =   
   4.100                   (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
   4.101  
   4.102    AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =   
   4.103 -	            (UN f:(PROD B:A. B). INT a:A. f`a))"
   4.104 +                    (UN f:(PROD B:A. B). INT a:A. f`a))"
   4.105  
   4.106  (* Auxiliary definitions used in the above definitions *)
   4.107  
   4.108    pairwise_disjoint_def    "pairwise_disjoint(A)   
   4.109 -			    == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
   4.110 +                            == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
   4.111  
   4.112    sets_of_size_between_def "sets_of_size_between(A,m,n)   
   4.113 -			    == ALL B:A. m lepoll B & B lepoll n"
   4.114 +                            == ALL B:A. m lepoll B & B lepoll n"
   4.115    
   4.116  end
     5.1 --- a/src/ZF/AC/DC.thy	Mon Feb 05 21:33:14 1996 +0100
     5.2 +++ b/src/ZF/AC/DC.thy	Tue Feb 06 12:27:17 1996 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4 -(*  Title: 	ZF/AC/DC.thy
     5.5 +(*  Title:      ZF/AC/DC.thy
     5.6      ID:         $Id$
     5.7 -    Author: 	Krzysztof Grabczewski
     5.8 +    Author:     Krzysztof Grabczewski
     5.9  
    5.10  Theory file for the proofs concernind the Axiom of Dependent Choice
    5.11  *)
    5.12 @@ -16,13 +16,13 @@
    5.13  rules
    5.14  
    5.15    DC_def  "DC(a) == ALL X R. R<=Pow(X)*X &
    5.16 -	   (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R)) 
    5.17 -	   --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
    5.18 +           (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R)) 
    5.19 +           --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
    5.20  
    5.21    DC0_def "DC0 == ALL A B R. R <= A*B & R~=0 & range(R) <= domain(R) 
    5.22 -	   --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
    5.23 +           --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
    5.24  
    5.25    ff_def  "ff(b, X, Q, R) == transrec(b, %c r. 
    5.26 -	                     THE x. first(x, {x:X. <r``c, x> : R}, Q))"
    5.27 +                             THE x. first(x, {x:X. <r``c, x> : R}, Q))"
    5.28    
    5.29  end
     6.1 --- a/src/ZF/AC/HH.thy	Mon Feb 05 21:33:14 1996 +0100
     6.2 +++ b/src/ZF/AC/HH.thy	Tue Feb 06 12:27:17 1996 +0100
     6.3 @@ -1,6 +1,6 @@
     6.4 -(*  Title: 	ZF/AC/HH.thy
     6.5 +(*  Title:      ZF/AC/HH.thy
     6.6      ID:         $Id$
     6.7 -    Author: 	Krzysztof Grabczewski
     6.8 +    Author:     Krzysztof Grabczewski
     6.9  
    6.10  The theory file for the proofs of
    6.11    AC17 ==> AC1
     7.1 --- a/src/ZF/AC/Hartog.thy	Mon Feb 05 21:33:14 1996 +0100
     7.2 +++ b/src/ZF/AC/Hartog.thy	Tue Feb 06 12:27:17 1996 +0100
     7.3 @@ -1,6 +1,6 @@
     7.4 -(*  Title: 	ZF/AC/Hartog.thy
     7.5 +(*  Title:      ZF/AC/Hartog.thy
     7.6      ID:         $Id$
     7.7 -    Author: 	Krzysztof Grabczewski
     7.8 +    Author:     Krzysztof Grabczewski
     7.9  
    7.10  Hartog's function.
    7.11  *)
     8.1 --- a/src/ZF/AC/OrdQuant.thy	Mon Feb 05 21:33:14 1996 +0100
     8.2 +++ b/src/ZF/AC/OrdQuant.thy	Tue Feb 06 12:27:17 1996 +0100
     8.3 @@ -1,6 +1,6 @@
     8.4 -(*  Title: 	ZF/AC/OrdQuant.thy
     8.5 +(*  Title:      ZF/AC/OrdQuant.thy
     8.6      ID:         $Id$
     8.7 -    Authors: 	Krzysztof Grabczewski and L C Paulson
     8.8 +    Authors:    Krzysztof Grabczewski and L C Paulson
     8.9  
    8.10  Quantifiers and union operator for ordinals. 
    8.11  *)
     9.1 --- a/src/ZF/AC/Transrec2.thy	Mon Feb 05 21:33:14 1996 +0100
     9.2 +++ b/src/ZF/AC/Transrec2.thy	Tue Feb 06 12:27:17 1996 +0100
     9.3 @@ -1,6 +1,6 @@
     9.4 -(*  Title: 	ZF/AC/Transrec2.thy
     9.5 +(*  Title:      ZF/AC/Transrec2.thy
     9.6      ID:         $Id$
     9.7 -    Author: 	Krzysztof Grabczewski
     9.8 +    Author:     Krzysztof Grabczewski
     9.9  
    9.10  Transfinite recursion introduced to handle definitions based on the three
    9.11  cases of ordinals.
    9.12 @@ -14,10 +14,10 @@
    9.13  
    9.14  defs
    9.15  
    9.16 -  transrec2_def  "transrec2(alpha, a, b) ==   			
    9.17 -		         transrec(alpha, %i r. if(i=0,   	
    9.18 -		                  a, if(EX j. i=succ(j),   	
    9.19 -		                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    9.20 -		                  UN j<i. r`j)))"
    9.21 +  transrec2_def  "transrec2(alpha, a, b) ==                     
    9.22 +                         transrec(alpha, %i r. if(i=0,          
    9.23 +                                  a, if(EX j. i=succ(j),        
    9.24 +                                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    9.25 +                                  UN j<i. r`j)))"
    9.26  
    9.27  end
    10.1 --- a/src/ZF/AC/WO6_WO1.thy	Mon Feb 05 21:33:14 1996 +0100
    10.2 +++ b/src/ZF/AC/WO6_WO1.thy	Tue Feb 06 12:27:17 1996 +0100
    10.3 @@ -1,6 +1,6 @@
    10.4 -(*  Title: 	ZF/AC/WO6_WO1.thy
    10.5 +(*  Title:      ZF/AC/WO6_WO1.thy
    10.6      ID:         $Id$
    10.7 -    Author: 	Krzysztof Grabczewski
    10.8 +    Author:     Krzysztof Grabczewski
    10.9  
   10.10  The proof of "WO6 ==> WO1".
   10.11  
   10.12 @@ -20,18 +20,18 @@
   10.13  defs
   10.14  
   10.15    NN_def  "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a  &  
   10.16 -			    (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
   10.17 +                            (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
   10.18  
   10.19    uu_def  "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
   10.20  
   10.21    (*Definitions for case 1*)
   10.22  
   10.23 -  vv1_def "vv1(f,m,b) ==   						
   10.24 -   	   let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &	
   10.25 -	                           domain(uu(f,b,g,d)) lepoll m));   	
   10.26 -	       d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &   		
   10.27 -                           domain(uu(f,b,g,d)) lepoll m		
   10.28 -	   in  if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
   10.29 +  vv1_def "vv1(f,m,b) ==                                                
   10.30 +           let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 & 
   10.31 +                                   domain(uu(f,b,g,d)) lepoll m));      
   10.32 +               d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &                  
   10.33 +                           domain(uu(f,b,g,d)) lepoll m         
   10.34 +           in  if(f`b ~= 0, domain(uu(f,b,g,d)), 0)"
   10.35  
   10.36    ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
   10.37  
   10.38 @@ -40,7 +40,7 @@
   10.39    (*Definitions for case 2*)
   10.40  
   10.41    vv2_def "vv2(f,b,g,s) ==   
   10.42 -	   if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
   10.43 +           if(f`g ~= 0, {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s}, 0)"
   10.44  
   10.45    ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
   10.46  
    11.1 --- a/src/ZF/AC/first.thy	Mon Feb 05 21:33:14 1996 +0100
    11.2 +++ b/src/ZF/AC/first.thy	Tue Feb 06 12:27:17 1996 +0100
    11.3 @@ -1,6 +1,6 @@
    11.4 -(*  Title: 	ZF/AC/first.thy
    11.5 +(*  Title:      ZF/AC/first.thy
    11.6      ID:         $Id$
    11.7 -    Author: 	Krzysztof Grabczewski
    11.8 +    Author:     Krzysztof Grabczewski
    11.9  
   11.10  Theory helpful in proofs using first element of a well ordered set
   11.11  *)
   11.12 @@ -14,5 +14,5 @@
   11.13  defs
   11.14  
   11.15    first_def                "first(u, X, R) 
   11.16 -			    == u:X & (ALL v:X. v~=u --> <u,v> : R)"
   11.17 +                            == u:X & (ALL v:X. v~=u --> <u,v> : R)"
   11.18  end
    12.1 --- a/src/ZF/AC/recfunAC16.thy	Mon Feb 05 21:33:14 1996 +0100
    12.2 +++ b/src/ZF/AC/recfunAC16.thy	Tue Feb 06 12:27:17 1996 +0100
    12.3 @@ -1,6 +1,6 @@
    12.4 -(*  Title: 	ZF/AC/recfunAC16.thy
    12.5 +(*  Title:      ZF/AC/recfunAC16.thy
    12.6      ID:         $Id$
    12.7 -    Author: 	Krzysztof Grabczewski
    12.8 +    Author:     Krzysztof Grabczewski
    12.9  
   12.10  A recursive definition used in the proof of WO2 ==> AC16
   12.11  *)
   12.12 @@ -15,9 +15,9 @@
   12.13  
   12.14    recfunAC16_def
   12.15      "recfunAC16(f,fa,i,a) == 
   12.16 -	 transrec2(i, 0, 
   12.17 -	      %g r. if(EX y:r. fa`g <= y, r, 
   12.18 -		       r Un {f`(LEAST i. fa`g <= f`i & 
   12.19 -		       (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
   12.20 +         transrec2(i, 0, 
   12.21 +              %g r. if(EX y:r. fa`g <= y, r, 
   12.22 +                       r Un {f`(LEAST i. fa`g <= f`i & 
   12.23 +                       (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
   12.24  
   12.25  end
    13.1 --- a/src/ZF/Arith.thy	Mon Feb 05 21:33:14 1996 +0100
    13.2 +++ b/src/ZF/Arith.thy	Tue Feb 06 12:27:17 1996 +0100
    13.3 @@ -1,6 +1,6 @@
    13.4 -(*  Title: 	ZF/arith.thy
    13.5 +(*  Title:      ZF/arith.thy
    13.6      ID:         $Id$
    13.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    13.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.9      Copyright   1992  University of Cambridge
   13.10  
   13.11  Arithmetic operators and their definitions
   13.12 @@ -9,11 +9,11 @@
   13.13  Arith = Epsilon + "simpdata" +
   13.14  consts
   13.15      rec  :: [i, i, [i,i]=>i]=>i
   13.16 -    "#*" :: [i,i]=>i      		(infixl 70)
   13.17 -    div  :: [i,i]=>i      		(infixl 70) 
   13.18 -    mod  :: [i,i]=>i      		(infixl 70)
   13.19 -    "#+" :: [i,i]=>i      		(infixl 65)
   13.20 -    "#-" :: [i,i]=>i      		(infixl 65)
   13.21 +    "#*" :: [i,i]=>i                    (infixl 70)
   13.22 +    div  :: [i,i]=>i                    (infixl 70) 
   13.23 +    mod  :: [i,i]=>i                    (infixl 70)
   13.24 +    "#+" :: [i,i]=>i                    (infixl 65)
   13.25 +    "#-" :: [i,i]=>i                    (infixl 65)
   13.26  
   13.27  defs
   13.28      rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
    14.1 --- a/src/ZF/Bool.thy	Mon Feb 05 21:33:14 1996 +0100
    14.2 +++ b/src/ZF/Bool.thy	Tue Feb 06 12:27:17 1996 +0100
    14.3 @@ -1,6 +1,6 @@
    14.4 -(*  Title: 	ZF/bool.thy
    14.5 +(*  Title:      ZF/bool.thy
    14.6      ID:         $Id$
    14.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    14.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.9      Copyright   1992  University of Cambridge
   14.10  
   14.11  Booleans in Zermelo-Fraenkel Set Theory 
   14.12 @@ -10,24 +10,24 @@
   14.13  
   14.14  Bool = ZF + "simpdata" +
   14.15  consts
   14.16 -    "1"		:: i     	   ("1")
   14.17 +    "1"         :: i               ("1")
   14.18      "2"         :: i             ("2")
   14.19      bool        :: i
   14.20      cond        :: [i,i,i]=>i
   14.21 -    not		:: i=>i
   14.22 +    not         :: i=>i
   14.23      "and"       :: [i,i]=>i      (infixl 70)
   14.24 -    or		:: [i,i]=>i      (infixl 65)
   14.25 -    xor		:: [i,i]=>i      (infixl 65)
   14.26 +    or          :: [i,i]=>i      (infixl 65)
   14.27 +    xor         :: [i,i]=>i      (infixl 65)
   14.28  
   14.29  translations
   14.30     "1"  == "succ(0)"
   14.31     "2"  == "succ(1)"
   14.32  
   14.33  defs
   14.34 -    bool_def	"bool == {0,1}"
   14.35 -    cond_def	"cond(b,c,d) == if(b=1,c,d)"
   14.36 -    not_def	"not(b) == cond(b,0,1)"
   14.37 -    and_def	"a and b == cond(a,b,0)"
   14.38 -    or_def	"a or b == cond(a,1,b)"
   14.39 -    xor_def	"a xor b == cond(a,not(b),b)"
   14.40 +    bool_def    "bool == {0,1}"
   14.41 +    cond_def    "cond(b,c,d) == if(b=1,c,d)"
   14.42 +    not_def     "not(b) == cond(b,0,1)"
   14.43 +    and_def     "a and b == cond(a,b,0)"
   14.44 +    or_def      "a or b == cond(a,1,b)"
   14.45 +    xor_def     "a xor b == cond(a,not(b),b)"
   14.46  end
    15.1 --- a/src/ZF/Cardinal.thy	Mon Feb 05 21:33:14 1996 +0100
    15.2 +++ b/src/ZF/Cardinal.thy	Tue Feb 06 12:27:17 1996 +0100
    15.3 @@ -1,6 +1,6 @@
    15.4 -(*  Title: 	ZF/Cardinal.thy
    15.5 +(*  Title:      ZF/Cardinal.thy
    15.6      ID:         $Id$
    15.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    15.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.9      Copyright   1994  University of Cambridge
   15.10  
   15.11  Cardinals in Zermelo-Fraenkel Set Theory 
    16.1 --- a/src/ZF/CardinalArith.thy	Mon Feb 05 21:33:14 1996 +0100
    16.2 +++ b/src/ZF/CardinalArith.thy	Tue Feb 06 12:27:17 1996 +0100
    16.3 @@ -1,6 +1,6 @@
    16.4 -(*  Title: 	ZF/CardinalArith.thy
    16.5 +(*  Title:      ZF/CardinalArith.thy
    16.6      ID:         $Id$
    16.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    16.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.9      Copyright   1994  University of Cambridge
   16.10  
   16.11  Cardinal Arithmetic
    17.1 --- a/src/ZF/Cardinal_AC.thy	Mon Feb 05 21:33:14 1996 +0100
    17.2 +++ b/src/ZF/Cardinal_AC.thy	Tue Feb 06 12:27:17 1996 +0100
    17.3 @@ -1,6 +1,6 @@
    17.4 -(*  Title: 	ZF/Cardinal_AC.thy
    17.5 +(*  Title:      ZF/Cardinal_AC.thy
    17.6      ID:         $Id$
    17.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    17.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.9      Copyright   1994  University of Cambridge
   17.10  
   17.11  Cardinal Arithmetic WITH the Axiom of Choice
    18.1 --- a/src/ZF/Coind/BCR.thy	Mon Feb 05 21:33:14 1996 +0100
    18.2 +++ b/src/ZF/Coind/BCR.thy	Tue Feb 06 12:27:17 1996 +0100
    18.3 @@ -1,6 +1,6 @@
    18.4 -(*  Title: 	ZF/Coind/BCR.thy
    18.5 +(*  Title:      ZF/Coind/BCR.thy
    18.6      ID:         $Id$
    18.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
    18.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
    18.9      Copyright   1995  University of Cambridge
   18.10  *)
   18.11  
   18.12 @@ -19,9 +19,9 @@
   18.13  consts
   18.14    isofenv :: [i,i] => o
   18.15  defs
   18.16 -  isofenv_def "isofenv(ve,te) ==   		
   18.17 -   ve_dom(ve) = te_dom(te) &   		
   18.18 -   ( ALL x:ve_dom(ve).   			
   18.19 +  isofenv_def "isofenv(ve,te) ==                
   18.20 +   ve_dom(ve) = te_dom(te) &            
   18.21 +   ( ALL x:ve_dom(ve).                          
   18.22       EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
   18.23    
   18.24  end
    19.1 --- a/src/ZF/Coind/Dynamic.thy	Mon Feb 05 21:33:14 1996 +0100
    19.2 +++ b/src/ZF/Coind/Dynamic.thy	Tue Feb 06 12:27:17 1996 +0100
    19.3 @@ -1,6 +1,6 @@
    19.4 -(*  Title: 	ZF/Coind/Dynamic.thy
    19.5 +(*  Title:      ZF/Coind/Dynamic.thy
    19.6      ID:         $Id$
    19.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
    19.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
    19.9      Copyright   1995  University of Cambridge
   19.10  *)
   19.11  
    20.1 --- a/src/ZF/Coind/ECR.thy	Mon Feb 05 21:33:14 1996 +0100
    20.2 +++ b/src/ZF/Coind/ECR.thy	Tue Feb 06 12:27:17 1996 +0100
    20.3 @@ -1,6 +1,6 @@
    20.4 -(*  Title: 	ZF/Coind/ECR.thy
    20.5 +(*  Title:      ZF/Coind/ECR.thy
    20.6      ID:         $Id$
    20.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
    20.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
    20.9      Copyright   1995  University of Cambridge
   20.10  *)
   20.11  
   20.12 @@ -17,9 +17,9 @@
   20.13        "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
   20.14      htr_closI
   20.15        "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; 
   20.16 -	  <te,e_fn(x,e),t>:ElabRel;  
   20.17 -	  ve_dom(ve) = te_dom(te);   
   20.18 -	  {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
   20.19 +          <te,e_fn(x,e),t>:ElabRel;  
   20.20 +          ve_dom(ve) = te_dom(te);   
   20.21 +          {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
   20.22        |] ==>   
   20.23        <v_clos(x,e,ve),t>:HasTyRel" 
   20.24    monos "[Pow_mono]"
   20.25 @@ -31,8 +31,8 @@
   20.26    hastyenv :: [i,i] => o
   20.27  defs
   20.28    hastyenv_def 
   20.29 -    " hastyenv(ve,te) == 			
   20.30 -     ve_dom(ve) = te_dom(te) & 		
   20.31 +    " hastyenv(ve,te) ==                        
   20.32 +     ve_dom(ve) = te_dom(te) &          
   20.33       (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
   20.34  
   20.35  end
    21.1 --- a/src/ZF/Coind/Language.thy	Mon Feb 05 21:33:14 1996 +0100
    21.2 +++ b/src/ZF/Coind/Language.thy	Tue Feb 06 12:27:17 1996 +0100
    21.3 @@ -1,14 +1,14 @@
    21.4 -(*  Title: 	ZF/Coind/Language.thy
    21.5 +(*  Title:      ZF/Coind/Language.thy
    21.6      ID:         $Id$
    21.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
    21.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
    21.9      Copyright   1995  University of Cambridge
   21.10  *)
   21.11  
   21.12  Language ="Datatype" + QUniv +
   21.13  
   21.14  consts
   21.15 -  Const :: i			(* Abstract type of constants *)
   21.16 -  c_app :: [i,i] => i		(*Abstract constructor for fun application*)
   21.17 +  Const :: i                    (* Abstract type of constants *)
   21.18 +  c_app :: [i,i] => i           (*Abstract constructor for fun application*)
   21.19  
   21.20  rules
   21.21    constNEE  "c:Const ==> c ~= 0"
   21.22 @@ -16,8 +16,8 @@
   21.23  
   21.24  
   21.25  consts
   21.26 -  Exp   :: i			(* Datatype of expressions *)
   21.27 -  ExVar :: i			(* Abstract type of variables *)
   21.28 +  Exp   :: i                    (* Datatype of expressions *)
   21.29 +  ExVar :: i                    (* Abstract type of variables *)
   21.30  datatype <= "univ(Const Un ExVar)"
   21.31    "Exp" = e_const("c:Const")
   21.32          | e_var("x:ExVar")
    22.1 --- a/src/ZF/Coind/Map.thy	Mon Feb 05 21:33:14 1996 +0100
    22.2 +++ b/src/ZF/Coind/Map.thy	Tue Feb 06 12:27:17 1996 +0100
    22.3 @@ -1,6 +1,6 @@
    22.4 -(*  Title: 	ZF/Coind/Map.thy
    22.5 +(*  Title:      ZF/Coind/Map.thy
    22.6      ID:         $Id$
    22.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
    22.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
    22.9      Copyright   1995  University of Cambridge
   22.10  *)
   22.11  
    23.1 --- a/src/ZF/Coind/Static.thy	Mon Feb 05 21:33:14 1996 +0100
    23.2 +++ b/src/ZF/Coind/Static.thy	Tue Feb 06 12:27:17 1996 +0100
    23.3 @@ -1,6 +1,6 @@
    23.4 -(*  Title: 	ZF/Coind/Static.thy
    23.5 +(*  Title:      ZF/Coind/Static.thy
    23.6      ID:         $Id$
    23.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
    23.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
    23.9      Copyright   1995  University of Cambridge
   23.10  *)
   23.11  
    24.1 --- a/src/ZF/Coind/Types.thy	Mon Feb 05 21:33:14 1996 +0100
    24.2 +++ b/src/ZF/Coind/Types.thy	Tue Feb 06 12:27:17 1996 +0100
    24.3 @@ -1,14 +1,14 @@
    24.4 -(*  Title: 	ZF/Coind/Types.thy
    24.5 +(*  Title:      ZF/Coind/Types.thy
    24.6      ID:         $Id$
    24.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
    24.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
    24.9      Copyright   1995  University of Cambridge
   24.10  *)
   24.11  
   24.12  Types = Language +
   24.13  
   24.14  consts
   24.15 -  Ty :: i			(* Datatype of types *)
   24.16 -  TyConst :: i		(* Abstract type of type constants *)
   24.17 +  Ty :: i                       (* Datatype of types *)
   24.18 +  TyConst :: i          (* Abstract type of type constants *)
   24.19  datatype <= "univ(TyConst)"
   24.20    "Ty" = t_const("tc:TyConst")
   24.21         | t_fun("t1:Ty","t2:Ty")
    25.1 --- a/src/ZF/Coind/Values.thy	Mon Feb 05 21:33:14 1996 +0100
    25.2 +++ b/src/ZF/Coind/Values.thy	Tue Feb 06 12:27:17 1996 +0100
    25.3 @@ -1,6 +1,6 @@
    25.4 -(*  Title: 	ZF/Coind/Values.thy
    25.5 +(*  Title:      ZF/Coind/Values.thy
    25.6      ID:         $Id$
    25.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
    25.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
    25.9      Copyright   1995  University of Cambridge
   25.10  *)
   25.11  
    26.1 --- a/src/ZF/Epsilon.thy	Mon Feb 05 21:33:14 1996 +0100
    26.2 +++ b/src/ZF/Epsilon.thy	Tue Feb 06 12:27:17 1996 +0100
    26.3 @@ -1,6 +1,6 @@
    26.4 -(*  Title: 	ZF/epsilon.thy
    26.5 +(*  Title:      ZF/epsilon.thy
    26.6      ID:         $Id$
    26.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    26.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    26.9      Copyright   1993  University of Cambridge
   26.10  
   26.11  Epsilon induction and recursion
   26.12 @@ -12,7 +12,7 @@
   26.13      transrec    ::      [i, [i,i]=>i] =>i
   26.14  
   26.15  defs
   26.16 -  eclose_def	"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
   26.17 -  transrec_def	"transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
   26.18 -  rank_def    	"rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
   26.19 +  eclose_def    "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
   26.20 +  transrec_def  "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
   26.21 +  rank_def      "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
   26.22  end
    27.1 --- a/src/ZF/EquivClass.thy	Mon Feb 05 21:33:14 1996 +0100
    27.2 +++ b/src/ZF/EquivClass.thy	Tue Feb 06 12:27:17 1996 +0100
    27.3 @@ -1,6 +1,6 @@
    27.4 -(*  Title: 	ZF/EquivClass.thy
    27.5 +(*  Title:      ZF/EquivClass.thy
    27.6      ID:         $Id$
    27.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    27.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    27.9      Copyright   1994  University of Cambridge
   27.10  
   27.11  Equivalence relations in Zermelo-Fraenkel Set Theory 
   27.12 @@ -9,7 +9,7 @@
   27.13  EquivClass = Rel + Perm + 
   27.14  consts
   27.15      "'/"        ::      [i,i]=>i  (infixl 90)  (*set of equiv classes*)
   27.16 -    congruent	::	[i,i=>i]=>o
   27.17 +    congruent   ::      [i,i=>i]=>o
   27.18      congruent2  ::      [i,[i,i]=>i]=>o
   27.19  
   27.20  defs
    28.1 --- a/src/ZF/Finite.thy	Mon Feb 05 21:33:14 1996 +0100
    28.2 +++ b/src/ZF/Finite.thy	Tue Feb 06 12:27:17 1996 +0100
    28.3 @@ -1,6 +1,6 @@
    28.4 -(*  Title: 	ZF/Finite.thy
    28.5 +(*  Title:      ZF/Finite.thy
    28.6      ID:         $Id$
    28.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    28.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    28.9      Copyright   1994  University of Cambridge
   28.10  
   28.11  Finite powerset operator
   28.12 @@ -8,8 +8,8 @@
   28.13  
   28.14  Finite = Arith + Inductive +
   28.15  consts
   28.16 -  Fin 	    :: i=>i
   28.17 -  FiniteFun :: [i,i]=>i		("(_ -||>/ _)" [61, 60] 60)
   28.18 +  Fin       :: i=>i
   28.19 +  FiniteFun :: [i,i]=>i         ("(_ -||>/ _)" [61, 60] 60)
   28.20  
   28.21  inductive
   28.22    domains   "Fin(A)" <= "Pow(A)"
   28.23 @@ -24,6 +24,6 @@
   28.24    intrs
   28.25      emptyI  "0 : A -||> B"
   28.26      consI   "[| a: A;  b: B;  h: A -||> B;  a ~: domain(h)   
   28.27 -	     |] ==> cons(<a,b>,h) : A -||> B"
   28.28 +             |] ==> cons(<a,b>,h) : A -||> B"
   28.29    type_intrs "Fin.intrs"
   28.30  end
    29.1 --- a/src/ZF/Fixedpt.thy	Mon Feb 05 21:33:14 1996 +0100
    29.2 +++ b/src/ZF/Fixedpt.thy	Tue Feb 06 12:27:17 1996 +0100
    29.3 @@ -1,6 +1,6 @@
    29.4 -(*  Title: 	ZF/fixedpt.thy
    29.5 +(*  Title:      ZF/fixedpt.thy
    29.6      ID:         $Id$
    29.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    29.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    29.9      Copyright   1992  University of Cambridge
   29.10  
   29.11  Least and greatest fixed points
    30.1 --- a/src/ZF/IMP/Com.thy	Mon Feb 05 21:33:14 1996 +0100
    30.2 +++ b/src/ZF/IMP/Com.thy	Tue Feb 06 12:27:17 1996 +0100
    30.3 @@ -1,6 +1,6 @@
    30.4 -(*  Title: 	ZF/IMP/Com.thy
    30.5 +(*  Title:      ZF/IMP/Com.thy
    30.6      ID:         $Id$
    30.7 -    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
    30.8 +    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
    30.9      Copyright   1994 TUM
   30.10  
   30.11  Arithmetic expressions, Boolean expressions, Commands
   30.12 @@ -23,14 +23,14 @@
   30.13  
   30.14  (** Evaluation of arithmetic expressions **)
   30.15  consts  evala    :: i
   30.16 -       "@evala"  :: [i,i,i] => o		("<_,_>/ -a-> _"  [0,0,50] 50)
   30.17 +       "@evala"  :: [i,i,i] => o                ("<_,_>/ -a-> _"  [0,0,50] 50)
   30.18  translations
   30.19      "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
   30.20  inductive
   30.21    domains "evala" <= "aexp * (loc -> nat) * nat"
   30.22    intrs 
   30.23      N   "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
   30.24 -    X  	"[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
   30.25 +    X   "[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
   30.26      Op1 "[| <e,sigma> -a-> n;  f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
   30.27      Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] 
   30.28             ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
   30.29 @@ -46,13 +46,13 @@
   30.30           | false
   30.31           | ROp  ("f: (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
   30.32           | noti ("b : bexp")
   30.33 -         | andi ("b0 : bexp", "b1 : bexp")	(infixl 60)
   30.34 -         | ori  ("b0 : bexp", "b1 : bexp")	(infixl 60)
   30.35 +         | andi ("b0 : bexp", "b1 : bexp")      (infixl 60)
   30.36 +         | ori  ("b0 : bexp", "b1 : bexp")      (infixl 60)
   30.37  
   30.38  
   30.39  (** Evaluation of boolean expressions **)
   30.40 -consts evalb	:: i	
   30.41 -       "@evalb" :: [i,i,i] => o		("<_,_>/ -b-> _" [0,0,50] 50)
   30.42 +consts evalb    :: i    
   30.43 +       "@evalb" :: [i,i,i] => o         ("<_,_>/ -b-> _" [0,0,50] 50)
   30.44  
   30.45  translations
   30.46      "<be,sig> -b-> b" == "<be,sig,b> : evalb"
   30.47 @@ -63,15 +63,15 @@
   30.48      tru   "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
   30.49      fls   "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
   30.50      ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] 
   30.51 -	   ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
   30.52 +           ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
   30.53      noti  "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
   30.54      andi  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
   30.55            ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
   30.56      ori   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
   30.57 -	    ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
   30.58 +            ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
   30.59  
   30.60    type_intrs "bexp.intrs @   
   30.61 -	      [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
   30.62 +              [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
   30.63    type_elims "[make_elim(evala.dom_subset RS subsetD)]"
   30.64  
   30.65  
   30.66 @@ -80,24 +80,24 @@
   30.67  
   30.68  datatype <= "univ(loc Un aexp Un bexp)"
   30.69    "com" = skip
   30.70 -        | ":="  ("x:loc", "a:aexp")		(infixl 60)
   30.71 -        | semic ("c0:com", "c1:com")		("_; _"  [60, 60] 10)
   30.72 -	| while ("b:bexp", "c:com")		("while _ do _"  60)
   30.73 -	| ifc   ("b:bexp", "c0:com", "c1:com")	("ifc _ then _ else _"  60)
   30.74 +        | ":="  ("x:loc", "a:aexp")             (infixl 60)
   30.75 +        | semic ("c0:com", "c1:com")            ("_; _"  [60, 60] 10)
   30.76 +        | while ("b:bexp", "c:com")             ("while _ do _"  60)
   30.77 +        | ifc   ("b:bexp", "c0:com", "c1:com")  ("ifc _ then _ else _"  60)
   30.78  
   30.79  (*Constructor ";" has low precedence to avoid syntactic ambiguities
   30.80    with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)
   30.81  
   30.82  (** Execution of commands **)
   30.83  consts  evalc    :: i
   30.84 -        "@evalc" :: [i,i,i] => o   		("<_,_>/ -c-> _" [0,0,50] 50)
   30.85 -	"assign" :: [i,i,i] => i   		("_[_'/_]"       [95,0,0] 95)
   30.86 +        "@evalc" :: [i,i,i] => o                ("<_,_>/ -c-> _" [0,0,50] 50)
   30.87 +        "assign" :: [i,i,i] => i                ("_[_'/_]"       [95,0,0] 95)
   30.88  
   30.89  translations
   30.90         "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
   30.91  
   30.92  defs 
   30.93 -	assign_def	"sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
   30.94 +        assign_def      "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
   30.95  
   30.96  inductive
   30.97    domains "evalc" <= "com * (loc -> nat) * (loc -> nat)"
   30.98 @@ -111,11 +111,11 @@
   30.99              <c0 ; c1, sigma> -c-> sigma1"
  30.100  
  30.101      ifc1     "[| b:bexp; c1:com; sigma:loc->nat;   
  30.102 -		 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> 
  30.103 +                 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> 
  30.104               <ifc b then c0 else c1, sigma> -c-> sigma1"
  30.105  
  30.106      ifc0     "[| b:bexp; c0:com; sigma:loc->nat;   
  30.107 -		 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> 
  30.108 +                 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> 
  30.109               <ifc b then c0 else c1, sigma> -c-> sigma1"
  30.110  
  30.111      while0   "[| c: com; <b, sigma> -b-> 0 |] ==> 
  30.112 @@ -128,6 +128,6 @@
  30.113    con_defs   "[assign_def]"
  30.114    type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
  30.115    type_elims "[make_elim(evala.dom_subset RS subsetD),   
  30.116 -	      make_elim(evalb.dom_subset RS subsetD) ]"
  30.117 +              make_elim(evalb.dom_subset RS subsetD) ]"
  30.118  
  30.119  end
    31.1 --- a/src/ZF/IMP/Denotation.thy	Mon Feb 05 21:33:14 1996 +0100
    31.2 +++ b/src/ZF/IMP/Denotation.thy	Tue Feb 06 12:27:17 1996 +0100
    31.3 @@ -1,6 +1,6 @@
    31.4 -(*  Title: 	ZF/IMP/Denotation.thy
    31.5 +(*  Title:      ZF/IMP/Denotation.thy
    31.6      ID:         $Id$
    31.7 -    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
    31.8 +    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
    31.9      Copyright   1994 TUM
   31.10  
   31.11  Denotational semantics of expressions & commands
   31.12 @@ -14,33 +14,33 @@
   31.13    C     :: i => i
   31.14    Gamma :: [i,i,i] => i
   31.15  
   31.16 -rules	(*NOT definitional*)
   31.17 -  A_nat_def	"A(N(n)) == (%sigma. n)"
   31.18 -  A_loc_def	"A(X(x)) == (%sigma. sigma`x)" 
   31.19 -  A_op1_def	"A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
   31.20 -  A_op2_def	"A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
   31.21 +rules   (*NOT definitional*)
   31.22 +  A_nat_def     "A(N(n)) == (%sigma. n)"
   31.23 +  A_loc_def     "A(X(x)) == (%sigma. sigma`x)" 
   31.24 +  A_op1_def     "A(Op1(f,a)) == (%sigma. f`A(a,sigma))"
   31.25 +  A_op2_def     "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)"
   31.26  
   31.27  
   31.28 -  B_true_def	"B(true) == (%sigma. 1)"
   31.29 -  B_false_def	"B(false) == (%sigma. 0)"
   31.30 -  B_op_def	"B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)" 
   31.31 +  B_true_def    "B(true) == (%sigma. 1)"
   31.32 +  B_false_def   "B(false) == (%sigma. 0)"
   31.33 +  B_op_def      "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)" 
   31.34  
   31.35  
   31.36 -  B_not_def	"B(noti(b)) == (%sigma. not(B(b,sigma)))"
   31.37 -  B_and_def	"B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
   31.38 -  B_or_def	"B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
   31.39 +  B_not_def     "B(noti(b)) == (%sigma. not(B(b,sigma)))"
   31.40 +  B_and_def     "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))"
   31.41 +  B_or_def      "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
   31.42  
   31.43 -  C_skip_def	"C(skip) == id(loc->nat)"
   31.44 -  C_assign_def	"C(x := a) == {io:(loc->nat)*(loc->nat). 
   31.45 -			       snd(io) = fst(io)[A(a,fst(io))/x]}"
   31.46 +  C_skip_def    "C(skip) == id(loc->nat)"
   31.47 +  C_assign_def  "C(x := a) == {io:(loc->nat)*(loc->nat). 
   31.48 +                               snd(io) = fst(io)[A(a,fst(io))/x]}"
   31.49  
   31.50 -  C_comp_def	"C(c0 ; c1) == C(c1) O C(c0)"
   31.51 -  C_if_def	"C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un 
   31.52 -			 	             {io:C(c1). B(b,fst(io))=0}"
   31.53 +  C_comp_def    "C(c0 ; c1) == C(c1) O C(c0)"
   31.54 +  C_if_def      "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un 
   31.55 +                                             {io:C(c1). B(b,fst(io))=0}"
   31.56  
   31.57 -  Gamma_def	"Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un 
   31.58 -			 	     {io : id(loc->nat). B(b,fst(io))=0})"
   31.59 +  Gamma_def     "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un 
   31.60 +                                     {io : id(loc->nat). B(b,fst(io))=0})"
   31.61  
   31.62 -  C_while_def	"C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
   31.63 +  C_while_def   "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))"
   31.64  
   31.65  end
    32.1 --- a/src/ZF/IMP/Equiv.thy	Mon Feb 05 21:33:14 1996 +0100
    32.2 +++ b/src/ZF/IMP/Equiv.thy	Tue Feb 06 12:27:17 1996 +0100
    32.3 @@ -1,6 +1,6 @@
    32.4 -(*  Title: 	ZF/IMP/Equiv.thy
    32.5 +(*  Title:      ZF/IMP/Equiv.thy
    32.6      ID:         $Id$
    32.7 -    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
    32.8 +    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
    32.9      Copyright   1994 TUM
   32.10  *)
   32.11  
    33.1 --- a/src/ZF/Let.thy	Mon Feb 05 21:33:14 1996 +0100
    33.2 +++ b/src/ZF/Let.thy	Tue Feb 06 12:27:17 1996 +0100
    33.3 @@ -1,6 +1,6 @@
    33.4 -(*  Title: 	ZF/Let
    33.5 +(*  Title:      ZF/Let
    33.6      ID:         $Id$
    33.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    33.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    33.9      Copyright   1995  University of Cambridge
   33.10  
   33.11  Let expressions, and tuple pattern-matching (borrowed from HOL)
    34.1 --- a/src/ZF/List.thy	Mon Feb 05 21:33:14 1996 +0100
    34.2 +++ b/src/ZF/List.thy	Tue Feb 06 12:27:17 1996 +0100
    34.3 @@ -1,6 +1,6 @@
    34.4 -(*  Title: 	ZF/List
    34.5 +(*  Title:      ZF/List
    34.6      ID:         $Id$
    34.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    34.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    34.9      Copyright   1994  University of Cambridge
   34.10  
   34.11  Lists in Zermelo-Fraenkel Set Theory 
   34.12 @@ -13,20 +13,20 @@
   34.13  List = Datatype + 
   34.14  
   34.15  consts
   34.16 -  "@"	     :: [i,i]=>i      			(infixr 60)
   34.17 +  "@"        :: [i,i]=>i                        (infixr 60)
   34.18    list_rec   :: [i, i, [i,i,i]=>i] => i
   34.19 -  map 	     :: [i=>i, i] => i
   34.20 +  map        :: [i=>i, i] => i
   34.21    length,rev :: i=>i
   34.22    flat       :: i=>i
   34.23    list_add   :: i=>i
   34.24    hd,tl      :: i=>i
   34.25 -  drop	     :: [i,i]=>i
   34.26 +  drop       :: [i,i]=>i
   34.27  
   34.28   (* List Enumeration *)
   34.29 - "[]"        :: i 	                           	("[]")
   34.30 - "@List"     :: is => i 	                   	("[(_)]")
   34.31 + "[]"        :: i                                       ("[]")
   34.32 + "@List"     :: is => i                                 ("[(_)]")
   34.33  
   34.34 -  list	     :: i=>i
   34.35 +  list       :: i=>i
   34.36  
   34.37    
   34.38  datatype
   34.39 @@ -41,9 +41,9 @@
   34.40  
   34.41  defs
   34.42  
   34.43 -  hd_def	"hd(l)	     == list_case(0, %x xs.x, l)"
   34.44 -  tl_def	"tl(l)       == list_case(Nil, %x xs.xs, l)"
   34.45 -  drop_def	"drop(i,l)   == rec(i, l, %j r. tl(r))"
   34.46 +  hd_def        "hd(l)       == list_case(0, %x xs.x, l)"
   34.47 +  tl_def        "tl(l)       == list_case(Nil, %x xs.xs, l)"
   34.48 +  drop_def      "drop(i,l)   == rec(i, l, %j r. tl(r))"
   34.49  
   34.50    list_rec_def
   34.51        "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
    35.1 --- a/src/ZF/Nat.thy	Mon Feb 05 21:33:14 1996 +0100
    35.2 +++ b/src/ZF/Nat.thy	Tue Feb 06 12:27:17 1996 +0100
    35.3 @@ -1,6 +1,6 @@
    35.4 -(*  Title: 	ZF/Nat.thy
    35.5 +(*  Title:      ZF/Nat.thy
    35.6      ID:         $Id$
    35.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    35.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    35.9      Copyright   1994  University of Cambridge
   35.10  
   35.11  Natural numbers in Zermelo-Fraenkel Set Theory 
   35.12 @@ -8,7 +8,7 @@
   35.13  
   35.14  Nat = Ordinal + Bool + "mono" +
   35.15  consts
   35.16 -    nat 	::      i
   35.17 +    nat         ::      i
   35.18      nat_case    ::      [i, i=>i, i]=>i
   35.19      nat_rec     ::      [i, i, [i,i]=>i]=>i
   35.20  
   35.21 @@ -17,10 +17,10 @@
   35.22      nat_def     "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
   35.23  
   35.24      nat_case_def
   35.25 -	"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
   35.26 +        "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
   35.27  
   35.28      nat_rec_def
   35.29 -	"nat_rec(k,a,b) ==   
   35.30 -   	  wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
   35.31 +        "nat_rec(k,a,b) ==   
   35.32 +          wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
   35.33  
   35.34  end
    36.1 --- a/src/ZF/Order.thy	Mon Feb 05 21:33:14 1996 +0100
    36.2 +++ b/src/ZF/Order.thy	Tue Feb 06 12:27:17 1996 +0100
    36.3 @@ -1,6 +1,6 @@
    36.4 -(*  Title: 	ZF/Order.thy
    36.5 +(*  Title:      ZF/Order.thy
    36.6      ID:         $Id$
    36.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    36.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    36.9      Copyright   1994  University of Cambridge
   36.10  
   36.11  Orders in Zermelo-Fraenkel Set Theory 
   36.12 @@ -8,13 +8,13 @@
   36.13  
   36.14  Order = WF + Perm + 
   36.15  consts
   36.16 -  part_ord        :: [i,i]=>o		(*Strict partial ordering*)
   36.17 -  linear, tot_ord :: [i,i]=>o		(*Strict total ordering*)
   36.18 -  well_ord        :: [i,i]=>o		(*Well-ordering*)
   36.19 -  mono_map        :: [i,i,i,i]=>i	(*Order-preserving maps*)
   36.20 -  ord_iso         :: [i,i,i,i]=>i	(*Order isomorphisms*)
   36.21 -  pred            :: [i,i,i]=>i	(*Set of predecessors*)
   36.22 -  ord_iso_map     :: [i,i,i,i]=>i	(*Construction for linearity theorem*)
   36.23 +  part_ord        :: [i,i]=>o           (*Strict partial ordering*)
   36.24 +  linear, tot_ord :: [i,i]=>o           (*Strict total ordering*)
   36.25 +  well_ord        :: [i,i]=>o           (*Well-ordering*)
   36.26 +  mono_map        :: [i,i,i,i]=>i       (*Order-preserving maps*)
   36.27 +  ord_iso         :: [i,i,i,i]=>i       (*Order isomorphisms*)
   36.28 +  pred            :: [i,i,i]=>i (*Set of predecessors*)
   36.29 +  ord_iso_map     :: [i,i,i,i]=>i       (*Construction for linearity theorem*)
   36.30  
   36.31  defs
   36.32    part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
    37.1 --- a/src/ZF/OrderArith.thy	Mon Feb 05 21:33:14 1996 +0100
    37.2 +++ b/src/ZF/OrderArith.thy	Tue Feb 06 12:27:17 1996 +0100
    37.3 @@ -1,6 +1,6 @@
    37.4 -(*  Title: 	ZF/OrderArith.thy
    37.5 +(*  Title:      ZF/OrderArith.thy
    37.6      ID:         $Id$
    37.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    37.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    37.9      Copyright   1994  University of Cambridge
   37.10  
   37.11  Towards ordinal arithmetic 
   37.12 @@ -15,14 +15,14 @@
   37.13    (*disjoint sum of two relations; underlies ordinal addition*)
   37.14    radd_def "radd(A,r,B,s) == 
   37.15                  {z: (A+B) * (A+B).  
   37.16 -                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 
   37.17 -                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 
   37.18 +                    (EX x y. z = <Inl(x), Inr(y)>)   |   
   37.19 +                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |      
   37.20                      (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
   37.21  
   37.22    (*lexicographic product of two relations; underlies ordinal multiplication*)
   37.23    rmult_def "rmult(A,r,B,s) == 
   37.24                  {z: (A*B) * (A*B).  
   37.25 -                    EX x' y' x y. z = <<x',y'>, <x,y>> &	 
   37.26 +                    EX x' y' x y. z = <<x',y'>, <x,y>> &         
   37.27                         (<x',x>: r | (x'=x & <y',y>: s))}"
   37.28  
   37.29    (*inverse image of a relation*)
    38.1 --- a/src/ZF/OrderType.thy	Mon Feb 05 21:33:14 1996 +0100
    38.2 +++ b/src/ZF/OrderType.thy	Tue Feb 06 12:27:17 1996 +0100
    38.3 @@ -1,6 +1,6 @@
    38.4 -(*  Title: 	ZF/OrderType.thy
    38.5 +(*  Title:      ZF/OrderType.thy
    38.6      ID:         $Id$
    38.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    38.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    38.9      Copyright   1994  University of Cambridge
   38.10  
   38.11  Order types and ordinal arithmetic.
    39.1 --- a/src/ZF/Ordinal.thy	Mon Feb 05 21:33:14 1996 +0100
    39.2 +++ b/src/ZF/Ordinal.thy	Tue Feb 06 12:27:17 1996 +0100
    39.3 @@ -1,6 +1,6 @@
    39.4 -(*  Title: 	ZF/Ordinal.thy
    39.5 +(*  Title:      ZF/Ordinal.thy
    39.6      ID:         $Id$
    39.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    39.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    39.9      Copyright   1994  University of Cambridge
   39.10  
   39.11  Ordinals in Zermelo-Fraenkel Set Theory 
   39.12 @@ -8,7 +8,7 @@
   39.13  
   39.14  Ordinal = WF + Bool + "simpdata" + "equalities" +
   39.15  consts
   39.16 -  Memrel      	:: i=>i
   39.17 +  Memrel        :: i=>i
   39.18    Transset,Ord  :: i=>o
   39.19    "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
   39.20    "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
   39.21 @@ -18,9 +18,9 @@
   39.22    "x le y"      == "x < succ(y)"
   39.23  
   39.24  defs
   39.25 -  Memrel_def  	"Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
   39.26 -  Transset_def	"Transset(i) == ALL x:i. x<=i"
   39.27 -  Ord_def     	"Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
   39.28 +  Memrel_def    "Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
   39.29 +  Transset_def  "Transset(i) == ALL x:i. x<=i"
   39.30 +  Ord_def       "Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
   39.31    lt_def        "i<j         == i:j & Ord(j)"
   39.32    Limit_def     "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
   39.33  
    40.1 --- a/src/ZF/Perm.thy	Mon Feb 05 21:33:14 1996 +0100
    40.2 +++ b/src/ZF/Perm.thy	Tue Feb 06 12:27:17 1996 +0100
    40.3 @@ -1,6 +1,6 @@
    40.4 -(*  Title: 	ZF/perm
    40.5 +(*  Title:      ZF/perm
    40.6      ID:         $Id$
    40.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    40.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    40.9      Copyright   1991  University of Cambridge
   40.10  
   40.11  The theory underlying permutation groups
   40.12 @@ -11,26 +11,26 @@
   40.13  
   40.14  Perm = ZF + "mono" +
   40.15  consts
   40.16 -    O    	::      [i,i]=>i      (infixr 60)
   40.17 -    id  	::      i=>i
   40.18 +    O           ::      [i,i]=>i      (infixr 60)
   40.19 +    id          ::      i=>i
   40.20      inj,surj,bij::      [i,i]=>i
   40.21  
   40.22  defs
   40.23  
   40.24      (*composition of relations and functions; NOT Suppes's relative product*)
   40.25 -    comp_def	"r O s == {xz : domain(s)*range(r) . 
   40.26 -                  		EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
   40.27 +    comp_def    "r O s == {xz : domain(s)*range(r) . 
   40.28 +                                EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
   40.29  
   40.30      (*the identity function for A*)
   40.31 -    id_def	"id(A) == (lam x:A. x)"
   40.32 +    id_def      "id(A) == (lam x:A. x)"
   40.33  
   40.34      (*one-to-one functions from A to B*)
   40.35      inj_def      "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
   40.36  
   40.37      (*onto functions from A to B*)
   40.38 -    surj_def	"surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
   40.39 +    surj_def    "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
   40.40  
   40.41      (*one-to-one and onto functions*)
   40.42 -    bij_def	"bij(A,B) == inj(A,B) Int surj(A,B)"
   40.43 +    bij_def     "bij(A,B) == inj(A,B) Int surj(A,B)"
   40.44  
   40.45  end
    41.1 --- a/src/ZF/QPair.thy	Mon Feb 05 21:33:14 1996 +0100
    41.2 +++ b/src/ZF/QPair.thy	Tue Feb 06 12:27:17 1996 +0100
    41.3 @@ -1,6 +1,6 @@
    41.4 -(*  Title: 	ZF/qpair.thy
    41.5 +(*  Title:      ZF/qpair.thy
    41.6      ID:         $Id$
    41.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    41.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    41.9      Copyright   1993  University of Cambridge
   41.10  
   41.11  Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
   41.12 @@ -13,19 +13,19 @@
   41.13  
   41.14  QPair = Sum + "simpdata" +
   41.15  consts
   41.16 -  QPair     :: [i, i] => i               	("<(_;/ _)>")
   41.17 +  QPair     :: [i, i] => i                      ("<(_;/ _)>")
   41.18    qfst,qsnd :: i => i
   41.19    qsplit    :: [[i, i] => 'a, i] => 'a::logic  (*for pattern-matching*)
   41.20    qconverse :: i => i
   41.21    QSigma    :: [i, i => i] => i
   41.22  
   41.23 -  "<+>"     :: [i,i]=>i      			(infixr 65)
   41.24 +  "<+>"     :: [i,i]=>i                         (infixr 65)
   41.25    QInl,QInr :: i=>i
   41.26    qcase     :: [i=>i, i=>i, i]=>i
   41.27  
   41.28  syntax
   41.29    "@QSUM"   :: [idt, i, i] => i               ("(3QSUM _:_./ _)" 10)
   41.30 -  "<*>"     :: [i, i] => i         		(infixr 80)
   41.31 +  "<*>"     :: [i, i] => i                      (infixr 80)
   41.32  
   41.33  translations
   41.34    "QSUM x:A. B"  => "QSigma(A, %x. B)"
    42.1 --- a/src/ZF/QUniv.thy	Mon Feb 05 21:33:14 1996 +0100
    42.2 +++ b/src/ZF/QUniv.thy	Tue Feb 06 12:27:17 1996 +0100
    42.3 @@ -1,6 +1,6 @@
    42.4 -(*  Title: 	ZF/univ.thy
    42.5 +(*  Title:      ZF/univ.thy
    42.6      ID:         $Id$
    42.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    42.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    42.9      Copyright   1993  University of Cambridge
   42.10  
   42.11  A small universe for lazy recursive types
    43.1 --- a/src/ZF/Rel.thy	Mon Feb 05 21:33:14 1996 +0100
    43.2 +++ b/src/ZF/Rel.thy	Tue Feb 06 12:27:17 1996 +0100
    43.3 @@ -1,6 +1,6 @@
    43.4 -(*  Title: 	ZF/Rel.thy
    43.5 +(*  Title:      ZF/Rel.thy
    43.6      ID:         $Id$
    43.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    43.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    43.9      Copyright   1994  University of Cambridge
   43.10  
   43.11  Relations in Zermelo-Fraenkel Set Theory 
   43.12 @@ -10,7 +10,7 @@
   43.13  consts
   43.14      refl,irrefl,equiv      :: [i,i]=>o
   43.15      sym,asym,antisym,trans :: i=>o
   43.16 -    trans_on               :: [i,i]=>o	("trans[_]'(_')")
   43.17 +    trans_on               :: [i,i]=>o  ("trans[_]'(_')")
   43.18  
   43.19  defs
   43.20    refl_def     "refl(A,r) == (ALL x: A. <x,x> : r)"
   43.21 @@ -25,7 +25,7 @@
   43.22  
   43.23    trans_def    "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
   43.24  
   43.25 -  trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. 	
   43.26 +  trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.       
   43.27                            <x,y>: r --> <y,z>: r --> <x,z>: r"
   43.28  
   43.29    equiv_def    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
    44.1 --- a/src/ZF/Resid/Confluence.thy	Mon Feb 05 21:33:14 1996 +0100
    44.2 +++ b/src/ZF/Resid/Confluence.thy	Tue Feb 06 12:27:17 1996 +0100
    44.3 @@ -1,6 +1,6 @@
    44.4 -(*  Title: 	Confluence.thy
    44.5 +(*  Title:      Confluence.thy
    44.6      ID:         $Id$
    44.7 -    Author: 	Ole Rasmussen
    44.8 +    Author:     Ole Rasmussen
    44.9      Copyright   1995  University of Cambridge
   44.10      Logic Image: ZF
   44.11  *)
   44.12 @@ -8,14 +8,14 @@
   44.13  Confluence = Reduction+
   44.14  
   44.15  consts
   44.16 -  confluence	:: i=>o
   44.17 -  strip		:: o
   44.18 +  confluence    :: i=>o
   44.19 +  strip         :: o
   44.20  
   44.21  defs
   44.22    confluence_def "confluence(R) ==   
   44.23 -		  ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->   
   44.24 -		                         (EX u.<y,u>:R & <z,u>:R))"
   44.25 +                  ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->   
   44.26 +                                         (EX u.<y,u>:R & <z,u>:R))"
   44.27    strip_def      "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->   
   44.28 -		                         (EX u.(y =1=> u) & (z===>u)))" 
   44.29 +                                         (EX u.(y =1=> u) & (z===>u)))" 
   44.30  end
   44.31  
    45.1 --- a/src/ZF/Resid/Conversion.thy	Mon Feb 05 21:33:14 1996 +0100
    45.2 +++ b/src/ZF/Resid/Conversion.thy	Tue Feb 06 12:27:17 1996 +0100
    45.3 @@ -1,6 +1,6 @@
    45.4 -(*  Title: 	Conversion.thy
    45.5 +(*  Title:      Conversion.thy
    45.6      ID:         $Id$
    45.7 -    Author: 	Ole Rasmussen
    45.8 +    Author:     Ole Rasmussen
    45.9      Copyright   1995  University of Cambridge
   45.10      Logic Image: ZF
   45.11  
   45.12 @@ -9,10 +9,10 @@
   45.13  Conversion = Confluence+
   45.14  
   45.15  consts
   45.16 -  Sconv1	:: i
   45.17 -  "<-1->"	:: [i,i]=>o (infixl 50)
   45.18 -  Sconv		:: i
   45.19 -  "<--->"	:: [i,i]=>o (infixl 50)
   45.20 +  Sconv1        :: i
   45.21 +  "<-1->"       :: [i,i]=>o (infixl 50)
   45.22 +  Sconv         :: i
   45.23 +  "<--->"       :: [i,i]=>o (infixl 50)
   45.24  
   45.25  translations
   45.26    "a<-1->b"    == "<a,b>:Sconv1"
   45.27 @@ -21,16 +21,16 @@
   45.28  inductive
   45.29    domains       "Sconv1" <= "lambda*lambda"
   45.30    intrs
   45.31 -    red1	"m -1-> n ==> m<-1->n"
   45.32 -    expl  	"n -1-> m ==> m<-1->n"
   45.33 -  type_intrs	"[red1D1,red1D2]@lambda.intrs@bool_typechecks"
   45.34 +    red1        "m -1-> n ==> m<-1->n"
   45.35 +    expl        "n -1-> m ==> m<-1->n"
   45.36 +  type_intrs    "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
   45.37  
   45.38  inductive
   45.39    domains       "Sconv" <= "lambda*lambda"
   45.40    intrs
   45.41 -    one_step	"m<-1->n  ==> m<--->n"
   45.42 -    refl  	"m:lambda ==> m<--->m"
   45.43 -    trans	"[|m<--->n; n<--->p|] ==> m<--->p"
   45.44 -  type_intrs	"[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
   45.45 +    one_step    "m<-1->n  ==> m<--->n"
   45.46 +    refl        "m:lambda ==> m<--->m"
   45.47 +    trans       "[|m<--->n; n<--->p|] ==> m<--->p"
   45.48 +  type_intrs    "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
   45.49  end
   45.50  
    46.1 --- a/src/ZF/Resid/Cube.thy	Mon Feb 05 21:33:14 1996 +0100
    46.2 +++ b/src/ZF/Resid/Cube.thy	Tue Feb 06 12:27:17 1996 +0100
    46.3 @@ -1,6 +1,6 @@
    46.4 -(*  Title: 	Cube.thy
    46.5 +(*  Title:      Cube.thy
    46.6      ID:         $Id$
    46.7 -    Author: 	Ole Rasmussen
    46.8 +    Author:     Ole Rasmussen
    46.9      Copyright   1995  University of Cambridge
   46.10      Logic Image: ZF
   46.11  *)
    47.1 --- a/src/ZF/Resid/Redex.thy	Mon Feb 05 21:33:14 1996 +0100
    47.2 +++ b/src/ZF/Resid/Redex.thy	Tue Feb 06 12:27:17 1996 +0100
    47.3 @@ -1,6 +1,6 @@
    47.4 -(*  Title: 	Redex.thy
    47.5 +(*  Title:      Redex.thy
    47.6      ID:         $Id$
    47.7 -    Author: 	Ole Rasmussen
    47.8 +    Author:     Ole Rasmussen
    47.9      Copyright   1995  University of Cambridge
   47.10      Logic Image: ZF
   47.11  *)
   47.12 @@ -10,14 +10,14 @@
   47.13    redexes     :: i
   47.14  
   47.15  datatype
   47.16 -  "redexes" = Var ("n: nat")	        
   47.17 +  "redexes" = Var ("n: nat")            
   47.18              | Fun ("t: redexes")
   47.19              | App ("b:bool" ,"f:redexes" , "a:redexes")
   47.20    type_intrs "[bool_into_univ]"
   47.21    
   47.22  
   47.23  consts
   47.24 -  redex_rec   	:: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
   47.25 +  redex_rec     :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
   47.26   
   47.27  defs
   47.28    redex_rec_def
    48.1 --- a/src/ZF/Resid/Reduction.thy	Mon Feb 05 21:33:14 1996 +0100
    48.2 +++ b/src/ZF/Resid/Reduction.thy	Tue Feb 06 12:27:17 1996 +0100
    48.3 @@ -1,6 +1,6 @@
    48.4 -(*  Title: 	Reduction.thy
    48.5 +(*  Title:      Reduction.thy
    48.6      ID:         $Id$
    48.7 -    Author: 	Ole Rasmussen
    48.8 +    Author:     Ole Rasmussen
    48.9      Copyright   1995  University of Cambridge
   48.10      Logic Image: ZF
   48.11  *)
   48.12 @@ -21,39 +21,39 @@
   48.13  inductive
   48.14    domains       "Sred1" <= "lambda*lambda"
   48.15    intrs
   48.16 -    beta	"[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
   48.17 -    rfun  	"[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
   48.18 -    apl_l	"[|m2:lambda; m1 -1-> n1|] ==>   
   48.19 -		 	          Apl(m1,m2) -1-> Apl(n1,m2)"
   48.20 -    apl_r	"[|m1:lambda; m2 -1-> n2|] ==>   
   48.21 -		 	          Apl(m1,m2) -1-> Apl(m1,n2)"
   48.22 -  type_intrs	"red_typechecks"
   48.23 +    beta        "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
   48.24 +    rfun        "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
   48.25 +    apl_l       "[|m2:lambda; m1 -1-> n1|] ==>   
   48.26 +                                  Apl(m1,m2) -1-> Apl(n1,m2)"
   48.27 +    apl_r       "[|m1:lambda; m2 -1-> n2|] ==>   
   48.28 +                                  Apl(m1,m2) -1-> Apl(m1,n2)"
   48.29 +  type_intrs    "red_typechecks"
   48.30  
   48.31  inductive
   48.32    domains       "Sred" <= "lambda*lambda"
   48.33    intrs
   48.34 -    one_step	"[|m-1->n|] ==> m--->n"
   48.35 -    refl  	"m:lambda==>m --->m"
   48.36 -    trans	"[|m--->n; n--->p|]==>m--->p"
   48.37 -  type_intrs	"[Sred1.dom_subset RS subsetD]@red_typechecks"
   48.38 +    one_step    "[|m-1->n|] ==> m--->n"
   48.39 +    refl        "m:lambda==>m --->m"
   48.40 +    trans       "[|m--->n; n--->p|]==>m--->p"
   48.41 +  type_intrs    "[Sred1.dom_subset RS subsetD]@red_typechecks"
   48.42  
   48.43  inductive
   48.44    domains       "Spar_red1" <= "lambda*lambda"
   48.45    intrs
   48.46 -    beta	"[|m =1=> m';   
   48.47 -		 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
   48.48 -    rvar	"n:nat==> Var(n) =1=> Var(n)"
   48.49 -    rfun	"[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
   48.50 -    rapl	"[|m =1=> m';   
   48.51 -		 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
   48.52 -  type_intrs	"red_typechecks"
   48.53 +    beta        "[|m =1=> m';   
   48.54 +                 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
   48.55 +    rvar        "n:nat==> Var(n) =1=> Var(n)"
   48.56 +    rfun        "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
   48.57 +    rapl        "[|m =1=> m';   
   48.58 +                 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
   48.59 +  type_intrs    "red_typechecks"
   48.60  
   48.61    inductive
   48.62    domains       "Spar_red" <= "lambda*lambda"
   48.63    intrs
   48.64 -    one_step	"[|m =1=> n|] ==> m ===> n"
   48.65 -    trans	"[|m===>n; n===>p|]==>m===>p"
   48.66 -  type_intrs	"[Spar_red1.dom_subset RS subsetD]@red_typechecks"
   48.67 +    one_step    "[|m =1=> n|] ==> m ===> n"
   48.68 +    trans       "[|m===>n; n===>p|]==>m===>p"
   48.69 +  type_intrs    "[Spar_red1.dom_subset RS subsetD]@red_typechecks"
   48.70  
   48.71  
   48.72  end
    49.1 --- a/src/ZF/Resid/Residuals.thy	Mon Feb 05 21:33:14 1996 +0100
    49.2 +++ b/src/ZF/Resid/Residuals.thy	Tue Feb 06 12:27:17 1996 +0100
    49.3 @@ -1,6 +1,6 @@
    49.4 -(*  Title: 	Residuals.thy
    49.5 +(*  Title:      Residuals.thy
    49.6      ID:         $Id$
    49.7 -    Author: 	Ole Rasmussen
    49.8 +    Author:     Ole Rasmussen
    49.9      Copyright   1995  University of Cambridge
   49.10      Logic Image: ZF
   49.11  
   49.12 @@ -9,9 +9,9 @@
   49.13  Residuals = Substitution+
   49.14  
   49.15  consts
   49.16 -  Sres		:: i
   49.17 -  residuals	:: [i,i,i]=>i
   49.18 -  "|>"		:: [i,i]=>i     (infixl 70)
   49.19 +  Sres          :: i
   49.20 +  residuals     :: [i,i,i]=>i
   49.21 +  "|>"          :: [i,i]=>i     (infixl 70)
   49.22    
   49.23  translations
   49.24    "residuals(u,v,w)"  == "<u,v,w>:Sres"
   49.25 @@ -19,16 +19,16 @@
   49.26  inductive
   49.27    domains       "Sres" <= "redexes*redexes*redexes"
   49.28    intrs
   49.29 -    Res_Var	"n:nat ==> residuals(Var(n),Var(n),Var(n))"
   49.30 -    Res_Fun	"[|residuals(u,v,w)|]==>   
   49.31 -		     residuals(Fun(u),Fun(v),Fun(w))"
   49.32 -    Res_App	"[|residuals(u1,v1,w1);   
   49.33 -		   residuals(u2,v2,w2); b:bool|]==>   
   49.34 -		 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
   49.35 -    Res_redex	"[|residuals(u1,v1,w1);   
   49.36 -		   residuals(u2,v2,w2); b:bool|]==>   
   49.37 -		 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
   49.38 -  type_intrs	"[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
   49.39 +    Res_Var     "n:nat ==> residuals(Var(n),Var(n),Var(n))"
   49.40 +    Res_Fun     "[|residuals(u,v,w)|]==>   
   49.41 +                     residuals(Fun(u),Fun(v),Fun(w))"
   49.42 +    Res_App     "[|residuals(u1,v1,w1);   
   49.43 +                   residuals(u2,v2,w2); b:bool|]==>   
   49.44 +                 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
   49.45 +    Res_redex   "[|residuals(u1,v1,w1);   
   49.46 +                   residuals(u2,v2,w2); b:bool|]==>   
   49.47 +                 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
   49.48 +  type_intrs    "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
   49.49  
   49.50  rules
   49.51    res_func_def  "u |> v == THE w.residuals(u,v,w)"
    50.1 --- a/src/ZF/Resid/SubUnion.thy	Mon Feb 05 21:33:14 1996 +0100
    50.2 +++ b/src/ZF/Resid/SubUnion.thy	Tue Feb 06 12:27:17 1996 +0100
    50.3 @@ -1,6 +1,6 @@
    50.4 -(*  Title: 	SubUnion.thy
    50.5 +(*  Title:      SubUnion.thy
    50.6      ID:         $Id$
    50.7 -    Author: 	Ole Rasmussen
    50.8 +    Author:     Ole Rasmussen
    50.9      Copyright   1995  University of Cambridge
   50.10      Logic Image: ZF
   50.11  *)
   50.12 @@ -11,7 +11,7 @@
   50.13    Ssub,Scomp,Sreg  :: i
   50.14    "<==","~"        :: [i,i]=>o (infixl 70)
   50.15    un               :: [i,i]=>i (infixl 70)
   50.16 -  regular	   :: i=>o
   50.17 +  regular          :: i=>o
   50.18    
   50.19  translations
   50.20    "a<==b"        == "<a,b>:Ssub"
   50.21 @@ -21,39 +21,39 @@
   50.22  inductive
   50.23    domains       "Ssub" <= "redexes*redexes"
   50.24    intrs
   50.25 -    Sub_Var	"n:nat ==> Var(n)<== Var(n)"
   50.26 -    Sub_Fun	"[|u<== v|]==> Fun(u)<== Fun(v)"
   50.27 -    Sub_App1	"[|u1<== v1; u2<== v2; b:bool|]==>   
   50.28 -		     App(0,u1,u2)<== App(b,v1,v2)"
   50.29 -    Sub_App2	"[|u1<== v1; u2<== v2|]==>   
   50.30 -		     App(1,u1,u2)<== App(1,v1,v2)"
   50.31 -  type_intrs	"redexes.intrs@bool_typechecks"
   50.32 +    Sub_Var     "n:nat ==> Var(n)<== Var(n)"
   50.33 +    Sub_Fun     "[|u<== v|]==> Fun(u)<== Fun(v)"
   50.34 +    Sub_App1    "[|u1<== v1; u2<== v2; b:bool|]==>   
   50.35 +                     App(0,u1,u2)<== App(b,v1,v2)"
   50.36 +    Sub_App2    "[|u1<== v1; u2<== v2|]==>   
   50.37 +                     App(1,u1,u2)<== App(1,v1,v2)"
   50.38 +  type_intrs    "redexes.intrs@bool_typechecks"
   50.39  
   50.40  inductive
   50.41    domains       "Scomp" <= "redexes*redexes"
   50.42    intrs
   50.43 -    Comp_Var	"n:nat ==> Var(n) ~ Var(n)"
   50.44 -    Comp_Fun	"[|u ~ v|]==> Fun(u) ~ Fun(v)"
   50.45 -    Comp_App	"[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>   
   50.46 -		     App(b1,u1,u2) ~ App(b2,v1,v2)"
   50.47 -  type_intrs	"redexes.intrs@bool_typechecks"
   50.48 +    Comp_Var    "n:nat ==> Var(n) ~ Var(n)"
   50.49 +    Comp_Fun    "[|u ~ v|]==> Fun(u) ~ Fun(v)"
   50.50 +    Comp_App    "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>   
   50.51 +                     App(b1,u1,u2) ~ App(b2,v1,v2)"
   50.52 +  type_intrs    "redexes.intrs@bool_typechecks"
   50.53  
   50.54  inductive
   50.55    domains       "Sreg" <= "redexes"
   50.56    intrs
   50.57 -    Reg_Var	"n:nat ==> regular(Var(n))"
   50.58 -    Reg_Fun	"[|regular(u)|]==> regular(Fun(u))"
   50.59 -    Reg_App1	"[|regular(Fun(u)); regular(v) 
   50.60 -		     |]==>regular(App(1,Fun(u),v))"
   50.61 -    Reg_App2	"[|regular(u); regular(v) 
   50.62 -		     |]==>regular(App(0,u,v))"
   50.63 -  type_intrs	"redexes.intrs@bool_typechecks"
   50.64 +    Reg_Var     "n:nat ==> regular(Var(n))"
   50.65 +    Reg_Fun     "[|regular(u)|]==> regular(Fun(u))"
   50.66 +    Reg_App1    "[|regular(Fun(u)); regular(v) 
   50.67 +                     |]==>regular(App(1,Fun(u),v))"
   50.68 +    Reg_App2    "[|regular(u); regular(v) 
   50.69 +                     |]==>regular(App(0,u,v))"
   50.70 +  type_intrs    "redexes.intrs@bool_typechecks"
   50.71  
   50.72  defs
   50.73    union_def  "u un v == redex_rec(u,   
   50.74 -	 %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),   
   50.75 +         %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),   
   50.76        %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),   
   50.77  %b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,   
   50.78 -	                               %c z u. App(b or c, m`z, p`u), t))`v"
   50.79 +                                       %c z u. App(b or c, m`z, p`u), t))`v"
   50.80  end
   50.81  
    51.1 --- a/src/ZF/Resid/Substitution.thy	Mon Feb 05 21:33:14 1996 +0100
    51.2 +++ b/src/ZF/Resid/Substitution.thy	Tue Feb 06 12:27:17 1996 +0100
    51.3 @@ -1,6 +1,6 @@
    51.4 -(*  Title: 	Substitution.thy
    51.5 +(*  Title:      Substitution.thy
    51.6      ID:         $Id$
    51.7 -    Author: 	Ole Rasmussen
    51.8 +    Author:     Ole Rasmussen
    51.9      Copyright   1995  University of Cambridge
   51.10      Logic Image: ZF
   51.11  *)
   51.12 @@ -8,19 +8,19 @@
   51.13  Substitution = SubUnion +
   51.14  
   51.15  consts
   51.16 -  lift_rec	:: [i,i]=> i
   51.17 -  lift		:: i=>i
   51.18 -  subst_rec	:: [i,i,i]=> i
   51.19 +  lift_rec      :: [i,i]=> i
   51.20 +  lift          :: i=>i
   51.21 +  subst_rec     :: [i,i,i]=> i
   51.22    "'/"          :: [i,i]=>i  (infixl 70)  (*subst*)
   51.23  translations
   51.24    "lift(r)"  == "lift_rec(r,0)"
   51.25    "u/v" == "subst_rec(u,v,0)"
   51.26    
   51.27  defs
   51.28 -  lift_rec_def	"lift_rec(r,kg) ==   
   51.29 -		     redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), 
   51.30 -		                 %x m.(lam k:nat.Fun(m`(succ(k)))),   
   51.31 -		                 %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
   51.32 +  lift_rec_def  "lift_rec(r,kg) ==   
   51.33 +                     redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), 
   51.34 +                                 %x m.(lam k:nat.Fun(m`(succ(k)))),   
   51.35 +                                 %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
   51.36  
   51.37    
   51.38  (* subst_rec(u,Var(i),k)     = if k<i then Var(i-1)
   51.39 @@ -30,15 +30,15 @@
   51.40     subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))
   51.41  
   51.42  *)
   51.43 -  subst_rec_def	"subst_rec(u,t,kg) ==   
   51.44 -		     redex_rec(t,   
   51.45 -		       %i.(lam r:redexes.lam k:nat.   
   51.46 -		              if(k<i,Var(i#-1),   
   51.47 -		                if(k=i,r,Var(i)))),   
   51.48 -		       %x m.(lam r:redexes.lam k:nat.   
   51.49 +  subst_rec_def "subst_rec(u,t,kg) ==   
   51.50 +                     redex_rec(t,   
   51.51 +                       %i.(lam r:redexes.lam k:nat.   
   51.52 +                              if(k<i,Var(i#-1),   
   51.53 +                                if(k=i,r,Var(i)))),   
   51.54 +                       %x m.(lam r:redexes.lam k:nat.   
   51.55                               Fun(m`(lift(r))`(succ(k)))),   
   51.56 -		       %b x y m p.lam r:redexes.lam k:nat.   
   51.57 -		              App(b,m`r`k,p`r`k))`u`kg"
   51.58 +                       %b x y m p.lam r:redexes.lam k:nat.   
   51.59 +                              App(b,m`r`k,p`r`k))`u`kg"
   51.60  
   51.61  
   51.62  end
    52.1 --- a/src/ZF/Resid/Terms.thy	Mon Feb 05 21:33:14 1996 +0100
    52.2 +++ b/src/ZF/Resid/Terms.thy	Tue Feb 06 12:27:17 1996 +0100
    52.3 @@ -1,6 +1,6 @@
    52.4 -(*  Title: 	Terms.thy
    52.5 +(*  Title:      Terms.thy
    52.6      ID:         $Id$
    52.7 -    Author: 	Ole Rasmussen
    52.8 +    Author:     Ole Rasmussen
    52.9      Copyright   1995  University of Cambridge
   52.10      Logic Image: ZF
   52.11  *)
   52.12 @@ -8,9 +8,9 @@
   52.13  Terms = Cube+
   52.14  
   52.15  consts
   52.16 -  lambda	:: i
   52.17 -  unmark	:: i=>i
   52.18 -  Apl		:: [i,i]=>i
   52.19 +  lambda        :: i
   52.20 +  unmark        :: i=>i
   52.21 +  Apl           :: [i,i]=>i
   52.22  
   52.23  translations
   52.24    "Apl(n,m)" == "App(0,n,m)"
   52.25 @@ -18,15 +18,15 @@
   52.26  inductive
   52.27    domains       "lambda" <= "redexes"
   52.28    intrs
   52.29 -    Lambda_Var	"               n:nat ==>     Var(n):lambda"
   52.30 -    Lambda_Fun	"            u:lambda ==>     Fun(u):lambda"
   52.31 -    Lambda_App	"[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
   52.32 -  type_intrs	"redexes.intrs@bool_typechecks"
   52.33 +    Lambda_Var  "               n:nat ==>     Var(n):lambda"
   52.34 +    Lambda_Fun  "            u:lambda ==>     Fun(u):lambda"
   52.35 +    Lambda_App  "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
   52.36 +  type_intrs    "redexes.intrs@bool_typechecks"
   52.37  
   52.38  defs
   52.39 -  unmark_def	"unmark(u) == redex_rec(u,%i.Var(i),   
   52.40 -		                          %x m.Fun(m),   
   52.41 -		                          %b x y m p.Apl(m,p))"
   52.42 +  unmark_def    "unmark(u) == redex_rec(u,%i.Var(i),   
   52.43 +                                          %x m.Fun(m),   
   52.44 +                                          %b x y m p.Apl(m,p))"
   52.45  end
   52.46  
   52.47  
    53.1 --- a/src/ZF/Sum.thy	Mon Feb 05 21:33:14 1996 +0100
    53.2 +++ b/src/ZF/Sum.thy	Tue Feb 06 12:27:17 1996 +0100
    53.3 @@ -1,6 +1,6 @@
    53.4 -(*  Title: 	ZF/sum.thy
    53.5 +(*  Title:      ZF/sum.thy
    53.6      ID:         $Id$
    53.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    53.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    53.9      Copyright   1993  University of Cambridge
   53.10  
   53.11  Disjoint sums in Zermelo-Fraenkel Set Theory 
   53.12 @@ -9,7 +9,7 @@
   53.13  
   53.14  Sum = Bool + "simpdata" +
   53.15  consts
   53.16 -    "+"    	:: [i,i]=>i      		(infixr 65)
   53.17 +    "+"         :: [i,i]=>i                     (infixr 65)
   53.18      Inl,Inr     :: i=>i
   53.19      case        :: [i=>i, i=>i, i]=>i
   53.20      Part        :: [i,i=>i] => i
   53.21 @@ -21,5 +21,5 @@
   53.22      case_def    "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"
   53.23  
   53.24    (*operator for selecting out the various summands*)
   53.25 -    Part_def	"Part(A,h) == {x: A. EX z. x = h(z)}"
   53.26 +    Part_def    "Part(A,h) == {x: A. EX z. x = h(z)}"
   53.27  end
    54.1 --- a/src/ZF/Trancl.thy	Mon Feb 05 21:33:14 1996 +0100
    54.2 +++ b/src/ZF/Trancl.thy	Tue Feb 06 12:27:17 1996 +0100
    54.3 @@ -1,6 +1,6 @@
    54.4 -(*  Title: 	ZF/trancl.thy
    54.5 +(*  Title:      ZF/trancl.thy
    54.6      ID:         $Id$
    54.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    54.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    54.9      Copyright   1992  University of Cambridge
   54.10  
   54.11  Transitive closure of a relation
   54.12 @@ -12,6 +12,6 @@
   54.13      trancl  :: i=>i  ("(_^+)" [100] 100)  (*transitive closure*)
   54.14  
   54.15  defs
   54.16 -    rtrancl_def	"r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
   54.17 +    rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
   54.18      trancl_def  "r^+ == r O r^*"
   54.19  end
    55.1 --- a/src/ZF/Univ.thy	Mon Feb 05 21:33:14 1996 +0100
    55.2 +++ b/src/ZF/Univ.thy	Tue Feb 06 12:27:17 1996 +0100
    55.3 @@ -1,6 +1,6 @@
    55.4 -(*  Title: 	ZF/univ.thy
    55.5 +(*  Title:      ZF/univ.thy
    55.6      ID:         $Id$
    55.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    55.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    55.9      Copyright   1992  University of Cambridge
   55.10  
   55.11  The cumulative hierarchy and a small universe for recursive types
   55.12 @@ -19,13 +19,13 @@
   55.13      univ        :: i=>i
   55.14  
   55.15  translations
   55.16 -    "Vset(x)"   == 	"Vfrom(0,x)"
   55.17 +    "Vset(x)"   ==      "Vfrom(0,x)"
   55.18  
   55.19  defs
   55.20      Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
   55.21  
   55.22      Vrec_def
   55.23 -   	"Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
   55.24 +        "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
   55.25                               H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
   55.26  
   55.27      univ_def    "univ(A) == Vfrom(A,nat)"
    56.1 --- a/src/ZF/WF.thy	Mon Feb 05 21:33:14 1996 +0100
    56.2 +++ b/src/ZF/WF.thy	Tue Feb 06 12:27:17 1996 +0100
    56.3 @@ -1,6 +1,6 @@
    56.4 -(*  Title: 	ZF/wf.thy
    56.5 +(*  Title:      ZF/wf.thy
    56.6      ID:         $Id$
    56.7 -    Author: 	Tobias Nipkow and Lawrence C Paulson
    56.8 +    Author:     Tobias Nipkow and Lawrence C Paulson
    56.9      Copyright   1994  University of Cambridge
   56.10  
   56.11  Well-founded Recursion
   56.12 @@ -9,26 +9,26 @@
   56.13  WF = Trancl + "mono" + "equalities" +
   56.14  consts
   56.15    wf           :: i=>o
   56.16 -  wf_on        :: [i,i]=>o			("wf[_]'(_')")
   56.17 +  wf_on        :: [i,i]=>o                      ("wf[_]'(_')")
   56.18  
   56.19    wftrec,wfrec :: [i, i, [i,i]=>i] =>i
   56.20 -  wfrec_on     :: [i, i, i, [i,i]=>i] =>i	("wfrec[_]'(_,_,_')")
   56.21 +  wfrec_on     :: [i, i, i, [i,i]=>i] =>i       ("wfrec[_]'(_,_,_')")
   56.22    is_recfun    :: [i, i, [i,i]=>i, i] =>o
   56.23    the_recfun   :: [i, i, [i,i]=>i] =>i
   56.24  
   56.25  defs
   56.26    (*r is a well-founded relation*)
   56.27 -  wf_def	 "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
   56.28 +  wf_def         "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
   56.29  
   56.30    (*r is well-founded relation over A*)
   56.31    wf_on_def      "wf_on(A,r) == wf(r Int A*A)"
   56.32  
   56.33    is_recfun_def  "is_recfun(r,a,H,f) == 
   56.34 -   			(f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
   56.35 +                        (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
   56.36  
   56.37    the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))"
   56.38  
   56.39 -  wftrec_def  	 "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
   56.40 +  wftrec_def     "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
   56.41  
   56.42    (*public version.  Does not require r to be transitive*)
   56.43    wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
    57.1 --- a/src/ZF/ZF.thy	Mon Feb 05 21:33:14 1996 +0100
    57.2 +++ b/src/ZF/ZF.thy	Tue Feb 06 12:27:17 1996 +0100
    57.3 @@ -61,7 +61,7 @@
    57.4    range       :: i => i
    57.5    field       :: i => i
    57.6    converse    :: i => i
    57.7 -  function    :: i => o	    	(*is a relation a function?*)
    57.8 +  function    :: i => o         (*is a relation a function?*)
    57.9    Lambda      :: [i, i => i] => i
   57.10    restrict    :: [i, i] => i
   57.11  
   57.12 @@ -214,8 +214,8 @@
   57.13    domain_def    "domain(r) == {x. w:r, EX y. w=<x,y>}"
   57.14    range_def     "range(r) == domain(converse(r))"
   57.15    field_def     "field(r) == domain(r) Un range(r)"
   57.16 -  function_def	"function(r) == ALL x y. <x,y>:r -->   
   57.17 -		                (ALL y'. <x,y'>:r --> y=y')"
   57.18 +  function_def  "function(r) == ALL x y. <x,y>:r -->   
   57.19 +                                (ALL y'. <x,y'>:r --> y=y')"
   57.20    image_def     "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
   57.21    vimage_def    "r -`` A == converse(r)``A"
   57.22  
    58.1 --- a/src/ZF/Zorn.thy	Mon Feb 05 21:33:14 1996 +0100
    58.2 +++ b/src/ZF/Zorn.thy	Tue Feb 06 12:27:17 1996 +0100
    58.3 @@ -1,6 +1,6 @@
    58.4 -(*  Title: 	ZF/Zorn.thy
    58.5 +(*  Title:      ZF/Zorn.thy
    58.6      ID:         $Id$
    58.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    58.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    58.9      Copyright   1994  University of Cambridge
   58.10  
   58.11  Based upon the article
   58.12 @@ -39,10 +39,10 @@
   58.13  inductive
   58.14    domains       "TFin(S,next)" <= "Pow(S)"
   58.15    intrs
   58.16 -    nextI	"[| x : TFin(S,next);  next: increasing(S) 
   58.17 +    nextI       "[| x : TFin(S,next);  next: increasing(S) 
   58.18                  |] ==> next`x : TFin(S,next)"
   58.19  
   58.20 -    Pow_UnionI	"Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
   58.21 +    Pow_UnionI  "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
   58.22  
   58.23    monos         "[Pow_mono]"
   58.24    con_defs      "[increasing_def]"
    59.1 --- a/src/ZF/ex/Acc.thy	Mon Feb 05 21:33:14 1996 +0100
    59.2 +++ b/src/ZF/ex/Acc.thy	Tue Feb 06 12:27:17 1996 +0100
    59.3 @@ -1,6 +1,6 @@
    59.4 -(*  Title: 	ZF/ex/Acc.thy
    59.5 +(*  Title:      ZF/ex/Acc.thy
    59.6      ID:         $Id$
    59.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    59.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    59.9      Copyright   1994  University of Cambridge
   59.10  
   59.11  Inductive definition of acc(r)
    60.1 --- a/src/ZF/ex/BT.thy	Mon Feb 05 21:33:14 1996 +0100
    60.2 +++ b/src/ZF/ex/BT.thy	Tue Feb 06 12:27:17 1996 +0100
    60.3 @@ -1,6 +1,6 @@
    60.4 -(*  Title: 	ZF/ex/BT.thy
    60.5 +(*  Title:      ZF/ex/BT.thy
    60.6      ID:         $Id$
    60.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    60.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    60.9      Copyright   1992  University of Cambridge
   60.10  
   60.11  Binary trees
   60.12 @@ -8,12 +8,12 @@
   60.13  
   60.14  BT = Datatype +
   60.15  consts
   60.16 -    bt_rec    	:: [i, i, [i,i,i,i,i]=>i] => i
   60.17 -    n_nodes	:: i=>i
   60.18 -    n_leaves   	:: i=>i
   60.19 -    bt_reflect 	:: i=>i
   60.20 +    bt_rec      :: [i, i, [i,i,i,i,i]=>i] => i
   60.21 +    n_nodes     :: i=>i
   60.22 +    n_leaves    :: i=>i
   60.23 +    bt_reflect  :: i=>i
   60.24  
   60.25 -    bt 	        :: i=>i
   60.26 +    bt          :: i=>i
   60.27  
   60.28  datatype
   60.29    "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
   60.30 @@ -22,8 +22,8 @@
   60.31    bt_rec_def
   60.32      "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
   60.33  
   60.34 -  n_nodes_def	"n_nodes(t) == bt_rec(t,  0,  %x y z r s. succ(r#+s))"
   60.35 -  n_leaves_def	"n_leaves(t) == bt_rec(t,  succ(0),  %x y z r s. r#+s)"
   60.36 +  n_nodes_def   "n_nodes(t) == bt_rec(t,  0,  %x y z r s. succ(r#+s))"
   60.37 +  n_leaves_def  "n_leaves(t) == bt_rec(t,  succ(0),  %x y z r s. r#+s)"
   60.38    bt_reflect_def "bt_reflect(t) == bt_rec(t,  Lf,  %x y z r s. Br(x,s,r))"
   60.39  
   60.40  end
    61.1 --- a/src/ZF/ex/Brouwer.thy	Mon Feb 05 21:33:14 1996 +0100
    61.2 +++ b/src/ZF/ex/Brouwer.thy	Tue Feb 06 12:27:17 1996 +0100
    61.3 @@ -1,6 +1,6 @@
    61.4 -(*  Title: 	ZF/ex/Brouwer.thy
    61.5 +(*  Title:      ZF/ex/Brouwer.thy
    61.6      ID:         $ $
    61.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    61.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    61.9      Copyright   1994  University of Cambridge
   61.10  
   61.11  Infinite branching datatype definitions
   61.12 @@ -15,15 +15,15 @@
   61.13   
   61.14  datatype <= "Vfrom(0, csucc(nat))"
   61.15    "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
   61.16 -  monos	      "[Pi_mono]"
   61.17 +  monos       "[Pi_mono]"
   61.18    type_intrs  "inf_datatype_intrs"
   61.19  
   61.20  (*The union with nat ensures that the cardinal is infinite*)
   61.21  datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
   61.22    "Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
   61.23 -  monos	      "[Pi_mono]"
   61.24 +  monos       "[Pi_mono]"
   61.25    type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   
   61.26 -	       @ inf_datatype_intrs"
   61.27 +               @ inf_datatype_intrs"
   61.28  
   61.29  
   61.30  end
    62.1 --- a/src/ZF/ex/CoUnit.thy	Mon Feb 05 21:33:14 1996 +0100
    62.2 +++ b/src/ZF/ex/CoUnit.thy	Tue Feb 06 12:27:17 1996 +0100
    62.3 @@ -1,6 +1,6 @@
    62.4 -(*  Title: 	ZF/ex/CoUnit.ML
    62.5 +(*  Title:      ZF/ex/CoUnit.ML
    62.6      ID:         $Id$
    62.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    62.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    62.9      Copyright   1994  University of Cambridge
   62.10  
   62.11  Trivial codatatype definitions, one of which goes wrong!
    63.1 --- a/src/ZF/ex/Comb.thy	Mon Feb 05 21:33:14 1996 +0100
    63.2 +++ b/src/ZF/ex/Comb.thy	Tue Feb 06 12:27:17 1996 +0100
    63.3 @@ -1,6 +1,6 @@
    63.4 -(*  Title: 	ZF/ex/Comb.thy
    63.5 +(*  Title:      ZF/ex/Comb.thy
    63.6      ID:         $Id$
    63.7 -    Author: 	Lawrence C Paulson
    63.8 +    Author:     Lawrence C Paulson
    63.9      Copyright   1994  University of Cambridge
   63.10  
   63.11  Combinatory Logic example: the Church-Rosser Theorem
   63.12 @@ -27,8 +27,8 @@
   63.13  **)
   63.14  consts
   63.15    contract  :: i
   63.16 -  "-1->"    :: [i,i] => o    			(infixl 50)
   63.17 -  "--->"    :: [i,i] => o    			(infixl 50)
   63.18 +  "-1->"    :: [i,i] => o                       (infixl 50)
   63.19 +  "--->"    :: [i,i] => o                       (infixl 50)
   63.20  
   63.21  translations
   63.22    "p -1-> q" == "<p,q> : contract"
   63.23 @@ -49,8 +49,8 @@
   63.24  **)
   63.25  consts
   63.26    parcontract :: i
   63.27 -  "=1=>"    :: [i,i] => o    			(infixl 50)
   63.28 -  "===>"    :: [i,i] => o    			(infixl 50)
   63.29 +  "=1=>"    :: [i,i] => o                       (infixl 50)
   63.30 +  "===>"    :: [i,i] => o                       (infixl 50)
   63.31  
   63.32  translations
   63.33    "p =1=> q" == "<p,q> : parcontract"
    64.1 --- a/src/ZF/ex/Data.thy	Mon Feb 05 21:33:14 1996 +0100
    64.2 +++ b/src/ZF/ex/Data.thy	Tue Feb 06 12:27:17 1996 +0100
    64.3 @@ -1,6 +1,6 @@
    64.4 -(*  Title: 	ZF/ex/Data.thy
    64.5 +(*  Title:      ZF/ex/Data.thy
    64.6      ID:         $Id$
    64.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    64.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    64.9      Copyright   1994  University of Cambridge
   64.10  
   64.11  Sample datatype definition.  
    65.1 --- a/src/ZF/ex/Enum.thy	Mon Feb 05 21:33:14 1996 +0100
    65.2 +++ b/src/ZF/ex/Enum.thy	Tue Feb 06 12:27:17 1996 +0100
    65.3 @@ -1,6 +1,6 @@
    65.4 -(*  Title: 	ZF/ex/Enum
    65.5 +(*  Title:      ZF/ex/Enum
    65.6      ID:         $Id$
    65.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    65.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    65.9      Copyright   1993  University of Cambridge
   65.10  
   65.11  Example of a BIG enumeration type
    66.1 --- a/src/ZF/ex/Integ.thy	Mon Feb 05 21:33:14 1996 +0100
    66.2 +++ b/src/ZF/ex/Integ.thy	Tue Feb 06 12:27:17 1996 +0100
    66.3 @@ -1,6 +1,6 @@
    66.4 -(*  Title: 	ZF/ex/integ.thy
    66.5 +(*  Title:      ZF/ex/integ.thy
    66.6      ID:         $Id$
    66.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    66.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    66.9      Copyright   1993  University of Cambridge
   66.10  
   66.11  The integers as equivalence classes over nat*nat.
   66.12 @@ -9,34 +9,34 @@
   66.13  Integ = EquivClass + Arith +
   66.14  consts
   66.15      intrel,integ::      i
   66.16 -    znat	::	i=>i		("$# _" [80] 80)
   66.17 -    zminus	::	i=>i		("$~ _" [80] 80)
   66.18 -    znegative	::	i=>o
   66.19 -    zmagnitude	::	i=>i
   66.20 +    znat        ::      i=>i            ("$# _" [80] 80)
   66.21 +    zminus      ::      i=>i            ("$~ _" [80] 80)
   66.22 +    znegative   ::      i=>o
   66.23 +    zmagnitude  ::      i=>i
   66.24      "$*"        ::      [i,i]=>i      (infixl 70)
   66.25      "$'/"       ::      [i,i]=>i      (infixl 70) 
   66.26      "$'/'/"     ::      [i,i]=>i      (infixl 70)
   66.27 -    "$+"	::      [i,i]=>i      (infixl 65)
   66.28 +    "$+"        ::      [i,i]=>i      (infixl 65)
   66.29      "$-"        ::      [i,i]=>i      (infixl 65)
   66.30 -    "$<"	:: 	[i,i]=>o  	(infixl 50)
   66.31 +    "$<"        ::      [i,i]=>o        (infixl 50)
   66.32  
   66.33  defs
   66.34  
   66.35      intrel_def
   66.36 -     "intrel == {p:(nat*nat)*(nat*nat). 		
   66.37 +     "intrel == {p:(nat*nat)*(nat*nat).                 
   66.38          EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
   66.39  
   66.40      integ_def   "integ == (nat*nat)/intrel"
   66.41      
   66.42 -    znat_def	"$# m == intrel `` {<m,0>}"
   66.43 +    znat_def    "$# m == intrel `` {<m,0>}"
   66.44      
   66.45 -    zminus_def	"$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
   66.46 +    zminus_def  "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
   66.47      
   66.48      znegative_def
   66.49 -	"znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
   66.50 +        "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
   66.51      
   66.52      zmagnitude_def
   66.53 -	"zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
   66.54 +        "zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
   66.55      
   66.56      (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
   66.57        Perhaps a "curried" or even polymorphic congruent predicate would be
   66.58 @@ -47,7 +47,7 @@
   66.59                             in intrel``{<x1#+x2, y1#+y2>}"
   66.60      
   66.61      zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
   66.62 -    zless_def	"Z1 $< Z2 == znegative(Z1 $- Z2)"
   66.63 +    zless_def   "Z1 $< Z2 == znegative(Z1 $- Z2)"
   66.64      
   66.65      (*This illustrates the primitive form of definitions (no patterns)*)
   66.66      zmult_def
    67.1 --- a/src/ZF/ex/LList.thy	Mon Feb 05 21:33:14 1996 +0100
    67.2 +++ b/src/ZF/ex/LList.thy	Tue Feb 06 12:27:17 1996 +0100
    67.3 @@ -1,6 +1,6 @@
    67.4 -(*  Title: 	ZF/ex/LList.thy
    67.5 +(*  Title:      ZF/ex/LList.thy
    67.6      ID:         $Id$
    67.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    67.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    67.9      Copyright   1994  University of Cambridge
   67.10  
   67.11  Codatatype definition of Lazy Lists
    68.1 --- a/src/ZF/ex/Limit.thy	Mon Feb 05 21:33:14 1996 +0100
    68.2 +++ b/src/ZF/ex/Limit.thy	Tue Feb 06 12:27:17 1996 +0100
    68.3 @@ -1,6 +1,6 @@
    68.4 -(*  Title: 	ZF/ex/Limit
    68.5 +(*  Title:      ZF/ex/Limit
    68.6      ID:         $Id$
    68.7 -    Author: 	Sten Agerholm
    68.8 +    Author:     Sten Agerholm
    68.9  
   68.10      A formalization of the inverse limit construction of domain theory.
   68.11  
    69.1 --- a/src/ZF/ex/ListN.thy	Mon Feb 05 21:33:14 1996 +0100
    69.2 +++ b/src/ZF/ex/ListN.thy	Tue Feb 06 12:27:17 1996 +0100
    69.3 @@ -1,6 +1,6 @@
    69.4 -(*  Title: 	ZF/ex/ListN
    69.5 +(*  Title:      ZF/ex/ListN
    69.6      ID:         $Id$
    69.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    69.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    69.9      Copyright   1994  University of Cambridge
   69.10  
   69.11  Inductive definition of lists of n elements
   69.12 @@ -10,7 +10,7 @@
   69.13  *)
   69.14  
   69.15  ListN = List +
   69.16 -consts	listn ::i=>i
   69.17 +consts  listn ::i=>i
   69.18  inductive
   69.19    domains   "listn(A)" <= "nat*list(A)"
   69.20    intrs
    70.1 --- a/src/ZF/ex/Ntree.thy	Mon Feb 05 21:33:14 1996 +0100
    70.2 +++ b/src/ZF/ex/Ntree.thy	Tue Feb 06 12:27:17 1996 +0100
    70.3 @@ -1,6 +1,6 @@
    70.4 -(*  Title: 	ZF/ex/Ntree.ML
    70.5 +(*  Title:      ZF/ex/Ntree.ML
    70.6      ID:         $Id$
    70.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    70.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    70.9      Copyright   1994  University of Cambridge
   70.10  
   70.11  Datatype definition n-ary branching trees
   70.12 @@ -17,18 +17,18 @@
   70.13  
   70.14  datatype
   70.15    "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
   70.16 -  monos	      "[[subset_refl, Pi_mono] MRS UN_mono]"	(*MUST have this form*)
   70.17 +  monos       "[[subset_refl, Pi_mono] MRS UN_mono]"    (*MUST have this form*)
   70.18    type_intrs  "[nat_fun_univ RS subsetD]"
   70.19    type_elims  "[UN_E]"
   70.20  
   70.21  datatype
   70.22    "maptree(A)" = Sons ("a: A", "h: maptree(A) -||> maptree(A)")
   70.23 -  monos	      "[FiniteFun_mono1]"	(*Use monotonicity in BOTH args*)
   70.24 +  monos       "[FiniteFun_mono1]"       (*Use monotonicity in BOTH args*)
   70.25    type_intrs  "[FiniteFun_univ1 RS subsetD]"
   70.26  
   70.27  datatype
   70.28    "maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
   70.29 -  monos	      "[subset_refl RS FiniteFun_mono]"
   70.30 +  monos       "[subset_refl RS FiniteFun_mono]"
   70.31    type_intrs  "[FiniteFun_in_univ']"
   70.32  
   70.33  end
    71.1 --- a/src/ZF/ex/Primrec.thy	Mon Feb 05 21:33:14 1996 +0100
    71.2 +++ b/src/ZF/ex/Primrec.thy	Tue Feb 06 12:27:17 1996 +0100
    71.3 @@ -1,6 +1,6 @@
    71.4 -(*  Title: 	ZF/ex/Primrec.thy
    71.5 +(*  Title:      ZF/ex/Primrec.thy
    71.6      ID:         $Id$
    71.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    71.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    71.9      Copyright   1994  University of Cambridge
   71.10  
   71.11  Primitive Recursive Functions
   71.12 @@ -22,8 +22,8 @@
   71.13      PROJ    :: i=>i
   71.14      COMP    :: [i,i]=>i
   71.15      PREC    :: [i,i]=>i
   71.16 -    ACK	    :: i=>i
   71.17 -    ack	    :: [i,i]=>i
   71.18 +    ACK     :: i=>i
   71.19 +    ack     :: [i,i]=>i
   71.20  
   71.21  translations
   71.22    "ack(x,y)"  == "ACK(x) ` [y]"
   71.23 @@ -57,8 +57,8 @@
   71.24      PREC     "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
   71.25    monos      "[list_mono]"
   71.26    con_defs   "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
   71.27 -  type_intrs "nat_typechecks @ list.intrs @   		        
   71.28 -	      [lam_type, list_case_type, drop_type, map_type,   
   71.29 -	      apply_type, rec_type]"
   71.30 +  type_intrs "nat_typechecks @ list.intrs @                     
   71.31 +              [lam_type, list_case_type, drop_type, map_type,   
   71.32 +              apply_type, rec_type]"
   71.33  
   71.34  end
    72.1 --- a/src/ZF/ex/PropLog.thy	Mon Feb 05 21:33:14 1996 +0100
    72.2 +++ b/src/ZF/ex/PropLog.thy	Tue Feb 06 12:27:17 1996 +0100
    72.3 @@ -1,6 +1,6 @@
    72.4 -(*  Title: 	ZF/ex/PropLog.thy
    72.5 +(*  Title:      ZF/ex/PropLog.thy
    72.6      ID:         $Id$
    72.7 -    Author: 	Tobias Nipkow & Lawrence C Paulson
    72.8 +    Author:     Tobias Nipkow & Lawrence C Paulson
    72.9      Copyright   1993  University of Cambridge
   72.10  
   72.11  Datatype definition of propositional logic formulae and inductive definition
   72.12 @@ -15,13 +15,13 @@
   72.13  
   72.14  datatype
   72.15    "prop" = Fls
   72.16 -         | Var ("n: nat")	                ("#_" [100] 100)
   72.17 -         | "=>" ("p: prop", "q: prop")		(infixr 90)
   72.18 +         | Var ("n: nat")                       ("#_" [100] 100)
   72.19 +         | "=>" ("p: prop", "q: prop")          (infixr 90)
   72.20  
   72.21  (** The proof system **)
   72.22  consts
   72.23    thms     :: i => i
   72.24 -  "|-"     :: [i,i] => o    			(infixl 50)
   72.25 +  "|-"     :: [i,i] => o                        (infixl 50)
   72.26  
   72.27  translations
   72.28    "H |- p" == "p : thms(H)"
   72.29 @@ -41,7 +41,7 @@
   72.30  consts
   72.31    prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
   72.32    is_true  :: [i,i] => o
   72.33 -  "|="     :: [i,i] => o    			(infixl 50)
   72.34 +  "|="     :: [i,i] => o                        (infixl 50)
   72.35    hyps     :: [i,i] => i
   72.36  
   72.37  defs
    73.1 --- a/src/ZF/ex/Ramsey.thy	Mon Feb 05 21:33:14 1996 +0100
    73.2 +++ b/src/ZF/ex/Ramsey.thy	Tue Feb 06 12:27:17 1996 +0100
    73.3 @@ -1,6 +1,6 @@
    73.4 -(*  Title: 	ZF/ex/ramsey.thy
    73.5 +(*  Title:      ZF/ex/ramsey.thy
    73.6      ID:         $Id$
    73.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    73.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    73.9      Copyright   1992  University of Cambridge
   73.10  
   73.11  Ramsey's Theorem (finite exponent 2 version)
   73.12 @@ -20,9 +20,9 @@
   73.13  
   73.14  Ramsey = Arith +
   73.15  consts
   73.16 -  Symmetric   		:: i=>o
   73.17 -  Atleast     		:: [i,i]=>o
   73.18 -  Clique,Indept,Ramsey	:: [i,i,i]=>o
   73.19 +  Symmetric             :: i=>o
   73.20 +  Atleast               :: [i,i]=>o
   73.21 +  Clique,Indept,Ramsey  :: [i,i,i]=>o
   73.22  
   73.23  defs
   73.24  
    74.1 --- a/src/ZF/ex/Rmap.thy	Mon Feb 05 21:33:14 1996 +0100
    74.2 +++ b/src/ZF/ex/Rmap.thy	Tue Feb 06 12:27:17 1996 +0100
    74.3 @@ -1,6 +1,6 @@
    74.4 -(*  Title: 	ZF/ex/Rmap
    74.5 +(*  Title:      ZF/ex/Rmap
    74.6      ID:         $Id$
    74.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    74.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    74.9      Copyright   1994  University of Cambridge
   74.10  
   74.11  Inductive definition of an operator to "map" a relation over a list
    75.1 --- a/src/ZF/ex/TF.thy	Mon Feb 05 21:33:14 1996 +0100
    75.2 +++ b/src/ZF/ex/TF.thy	Tue Feb 06 12:27:17 1996 +0100
    75.3 @@ -1,6 +1,6 @@
    75.4 -(*  Title: 	ZF/ex/TF.thy
    75.5 +(*  Title:      ZF/ex/TF.thy
    75.6      ID:         $Id$
    75.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    75.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    75.9      Copyright   1994  University of Cambridge
   75.10  
   75.11  Trees & forests, a mutually recursive type definition.
   75.12 @@ -24,14 +24,14 @@
   75.13  
   75.14  defs
   75.15    TF_rec_def
   75.16 -    "TF_rec(z,b,c,d) == Vrec(z,  			
   75.17 -      %z r. tree_forest_case(%x f. b(x, f, r`f), 	
   75.18 -                             c, 			
   75.19 -		              %t f. d(t, f, r`t, r`f), z))"
   75.20 +    "TF_rec(z,b,c,d) == Vrec(z,                         
   75.21 +      %z r. tree_forest_case(%x f. b(x, f, r`f),        
   75.22 +                             c,                         
   75.23 +                              %t f. d(t, f, r`t, r`f), z))"
   75.24  
   75.25    list_of_TF_def
   75.26      "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], 
   75.27 -		             %t f r1 r2. Cons(t, r2))"
   75.28 +                             %t f r1 r2. Cons(t, r2))"
   75.29  
   75.30    TF_of_list_def
   75.31      "TF_of_list(f) == list_rec(f, Fnil,  %t f r. Fcons(t,r))"
    76.1 --- a/src/ZF/ex/Term.thy	Mon Feb 05 21:33:14 1996 +0100
    76.2 +++ b/src/ZF/ex/Term.thy	Tue Feb 06 12:27:17 1996 +0100
    76.3 @@ -1,6 +1,6 @@
    76.4 -(*  Title: 	ZF/ex/Term.thy
    76.5 +(*  Title:      ZF/ex/Term.thy
    76.6      ID:         $Id$
    76.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    76.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    76.9      Copyright   1994  University of Cambridge
   76.10  
   76.11  Terms over an alphabet.
   76.12 @@ -19,7 +19,7 @@
   76.13  
   76.14  datatype
   76.15    "term(A)" = Apply ("a: A", "l: list(term(A))")
   76.16 -  monos	      "[list_mono]"
   76.17 +  monos       "[list_mono]"
   76.18  
   76.19    type_elims  "[make_elim (list_univ RS subsetD)]"
   76.20  (*Or could have
   76.21 @@ -31,12 +31,12 @@
   76.22     "term_rec(t,d) == 
   76.23     Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
   76.24  
   76.25 -  term_map_def	"term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
   76.26 +  term_map_def  "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
   76.27  
   76.28 -  term_size_def	"term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
   76.29 +  term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
   76.30  
   76.31 -  reflect_def	"reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
   76.32 +  reflect_def   "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
   76.33  
   76.34 -  preorder_def	"preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
   76.35 +  preorder_def  "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
   76.36  
   76.37  end
    77.1 --- a/src/ZF/ex/twos_compl.thy	Mon Feb 05 21:33:14 1996 +0100
    77.2 +++ b/src/ZF/ex/twos_compl.thy	Tue Feb 06 12:27:17 1996 +0100
    77.3 @@ -1,5 +1,5 @@
    77.4  (*  ID:         $Id$
    77.5 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    77.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    77.7      Copyright   1994  University of Cambridge
    77.8  *)
    77.9