--- a/Arith.ML Wed Dec 14 10:32:07 1994 +0100
+++ b/Arith.ML Wed Dec 14 11:17:18 1994 +0100
@@ -189,7 +189,7 @@
qed "diffs0_imp_equal_lemma";
(* [| m-n = 0; n-m = 0 |] ==> m=n *)
-val diffs0_imp_equal = standard (diffs0_imp_equal_lemma RS mp RS mp);
+bind_thm ("diffs0_imp_equal", (diffs0_imp_equal_lemma RS mp RS mp));
val [prem] = goal Arith.thy "m<n ==> 0<n-m";
by (rtac (prem RS rev_mp) 1);
@@ -235,8 +235,8 @@
by (rtac le_add2 1);
qed "le_add1";
-val less_add_Suc1 = standard (lessI RS (le_add1 RS le_less_trans));
-val less_add_Suc2 = standard (lessI RS (le_add2 RS le_less_trans));
+bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
+bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
goal Arith.thy "m+k<=n --> m<=(n::nat)";
by (nat_ind_tac "k" 1);