# HG changeset patch
# User paulson
# Date 932999543 -7200
# Node ID f9aa63a5a8b65a7f22dc048ef3d9b361fcd3819b
# Parent  e5a5f8d23f262f0c1b431cce15127d407e01ea92
expandshort

diff -r e5a5f8d23f26 -r f9aa63a5a8b6 src/HOL/Integ/IntDiv.ML
--- 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";
diff -r e5a5f8d23f26 -r f9aa63a5a8b6 src/HOL/Integ/NatBin.ML
--- 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";