--- a/src/HOL/Arith.ML Wed Nov 05 13:27:58 1997 +0100
+++ b/src/HOL/Arith.ML Wed Nov 05 13:29:47 1997 +0100
@@ -35,12 +35,12 @@
AddIffs [pred_le];
goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
-by(simp_tac (simpset() addsplits [expand_nat_case]) 1);
+by (simp_tac (simpset() addsplits [expand_nat_case]) 1);
qed_spec_mp "pred_le_mono";
goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
-by(exhaust_tac "n" 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (exhaust_tac "n" 1);
+by (ALLGOALS Asm_full_simp_tac);
qed "pred_less";
Addsimps [pred_less];
@@ -327,6 +327,12 @@
qed "mult_is_0";
Addsimps [mult_is_0];
+goal Arith.thy "!!m::nat. m <= m*m";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
+by (etac (le_add2 RSN (2,le_trans)) 1);
+qed "le_square";
+
(*** Difference ***)