ASCII-fied;
authorwenzelm
Mon Nov 10 15:25:12 1997 +0100 (1997-11-10)
changeset 41957f7bf0bd0f63
parent 4194 1c2553be1821
child 4196 9953c0995b79
ASCII-fied;
src/HOL/Integ/Bin.ML
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Integ.ML
     1.1 --- a/src/HOL/Integ/Bin.ML	Mon Nov 10 15:06:58 1997 +0100
     1.2 +++ b/src/HOL/Integ/Bin.ML	Mon Nov 10 15:25:12 1997 +0100
     1.3 @@ -193,7 +193,7 @@
     1.4            norm_Bcons_Bcons];
     1.5  
     1.6  
     1.7 -(** Simplification rules for comparison of binary numbers (Norbert Völker) **) 
     1.8 +(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) 
     1.9  
    1.10  Addsimps [zadd_assoc];
    1.11  
     2.1 --- a/src/HOL/Integ/Equiv.ML	Mon Nov 10 15:06:58 1997 +0100
     2.2 +++ b/src/HOL/Integ/Equiv.ML	Mon Nov 10 15:25:12 1997 +0100
     2.3 @@ -241,7 +241,7 @@
     2.4  qed "congruent2_commuteI";
     2.5  
     2.6  
     2.7 -(*** Cardinality results suggested by Florian Kammüller ***)
     2.8 +(*** Cardinality results suggested by Florian Kammueller ***)
     2.9  
    2.10  (*Recall that  equiv A r  implies  r <= A Times A   (equiv_type) *)
    2.11  goal thy "!!A. [| finite A; r <= A Times A |] ==> finite (A/r)";
     3.1 --- a/src/HOL/Integ/Integ.ML	Mon Nov 10 15:06:58 1997 +0100
     3.2 +++ b/src/HOL/Integ/Integ.ML	Mon Nov 10 15:25:12 1997 +0100
     3.3 @@ -757,7 +757,7 @@
     3.4  qed "zadd_zle_self";
     3.5  
     3.6  
     3.7 -(**** Comparisons: lemmas and proofs by Norbert Völker ****)
     3.8 +(**** Comparisons: lemmas and proofs by Norbert Voelker ****)
     3.9  
    3.10  (** One auxiliary theorem...**)
    3.11