src/HOL/NatArith.ML
changeset 11468 02cd5d5bc497
parent 11451 8abfb4f7bd02
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/NatArith.ML	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/NatArith.ML	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -96,17 +96,17 @@
     1.4  
     1.5  (** Lemmas for ex/Factorization **)
     1.6  
     1.7 -Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
     1.8 +Goal "!!m::nat. [| 1' < n; 1' < m |] ==> 1' < m*n";
     1.9  by (case_tac "m" 1);
    1.10  by Auto_tac;
    1.11  qed "one_less_mult"; 
    1.12  
    1.13 -Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
    1.14 +Goal "!!m::nat. [| 1' < n; 1' < m |] ==> n<m*n";
    1.15  by (case_tac "m" 1);
    1.16  by Auto_tac;
    1.17  qed "n_less_m_mult_n"; 
    1.18  
    1.19 -Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
    1.20 +Goal "!!m::nat. [| 1' < n; 1' < m |] ==> n<n*m";
    1.21  by (case_tac "m" 1);
    1.22  by Auto_tac;
    1.23  qed "n_less_n_mult_m";