--- a/src/HOL/NatArith.ML Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/NatArith.ML Tue Aug 07 16:36:52 2001 +0200
@@ -96,17 +96,17 @@
(** Lemmas for ex/Factorization **)
-Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
+Goal "!!m::nat. [| 1' < n; 1' < m |] ==> 1' < 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. [| 1' < n; 1' < 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. [| 1' < n; 1' < m |] ==> n<n*m";
by (case_tac "m" 1);
by Auto_tac;
qed "n_less_n_mult_m";