--- a/src/HOL/Integ/IntDiv.ML Mon Jul 26 16:30:50 1999 +0200
+++ b/src/HOL/Integ/IntDiv.ML Mon Jul 26 16:32:23 1999 +0200
@@ -908,7 +908,7 @@
by (asm_full_simp_tac (HOL_ss
addsimps [zmod_zminus_zminus, zdiff_def,
zminus_zadd_distrib RS sym]) 1);
-bd (zminus_equation RS iffD1 RS sym) 1;
+by (dtac (zminus_equation RS iffD1 RS sym) 1);
by (auto_tac (claset(),
simpset() addsimps [zmult_zminus_right]));
qed "neg_zmod_times_2";
--- a/src/HOL/Integ/NatBin.ML Mon Jul 26 16:30:50 1999 +0200
+++ b/src/HOL/Integ/NatBin.ML Mon Jul 26 16:32:23 1999 +0200
@@ -44,7 +44,7 @@
(** Successor **)
Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
-br sym 1;
+by (rtac sym 1);
by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
qed "Suc_nat_eq_nat_zadd1";