--- a/Nat.ML Wed Dec 14 10:32:07 1994 +0100
+++ b/Nat.ML Wed Dec 14 11:17:18 1994 +0100
@@ -95,9 +95,9 @@
by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
qed "Suc_not_Zero";
-val Zero_not_Suc = standard (Suc_not_Zero RS not_sym);
+bind_thm ("Zero_not_Suc", (Suc_not_Zero RS not_sym));
-val Suc_neq_Zero = standard (Suc_not_Zero RS notE);
+bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
val Zero_neq_Suc = sym RS Suc_neq_Zero;
(** Injectiveness of Suc **)
@@ -158,7 +158,7 @@
(*** nat_rec -- by wf recursion on pred_nat ***)
-val nat_rec_unfold = standard (wf_pred_nat RS (nat_rec_def RS def_wfrec));
+bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec)));
(** conversion rules **)
@@ -221,7 +221,7 @@
qed "less_not_sym";
(* [| n<m; m<n |] ==> R *)
-val less_asym = standard (less_not_sym RS notE);
+bind_thm ("less_asym", (less_not_sym RS notE));
goalw Nat.thy [less_def] "~ n<(n::nat)";
by (rtac notI 1);
@@ -229,7 +229,7 @@
qed "less_not_refl";
(* n<n ==> R *)
-val less_anti_refl = standard (less_not_refl RS notE);
+bind_thm ("less_anti_refl", (less_not_refl RS notE));
goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
by(fast_tac (HOL_cs addEs [less_anti_refl]) 1);
@@ -252,7 +252,7 @@
qed "not_less0";
(* n<0 ==> R *)
-val less_zeroE = standard (not_less0 RS notE);
+bind_thm ("less_zeroE", (not_less0 RS notE));
val [major,less,eq] = goal Nat.thy
"[| m < Suc(n); m<n ==> P; m=n ==> P |] ==> P";