src/HOL/NatArith.ML

--- a/src/HOL/NatArith.ML	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/NatArith.ML	Fri Oct 05 21:52:39 2001 +0200
@@ -96,17 +96,17 @@
 
 (** Lemmas for ex/Factorization **)
 
-Goal "!!m::nat. [| 1' < n; 1' < m |] ==> 1' < m*n";
+Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n";
 by (case_tac "m" 1);
 by Auto_tac;
 qed "one_less_mult"; 
 
-Goal "!!m::nat. [| 1' < n; 1' < m |] ==> n<m*n";
+Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> n<m*n";
 by (case_tac "m" 1);
 by Auto_tac;
 qed "n_less_m_mult_n"; 
 
-Goal "!!m::nat. [| 1' < n; 1' < m |] ==> n<n*m";
+Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> n<n*m";
 by (case_tac "m" 1);
 by Auto_tac;
 qed "n_less_n_mult_m";