expandshort
authorpaulson
Mon Jul 26 16:32:23 1999 +0200 (1999-07-26)
changeset 7086f9aa63a5a8b6
parent 7085 e5a5f8d23f26
child 7087 67c6706578ed
expandshort
src/HOL/Integ/IntDiv.ML
src/HOL/Integ/NatBin.ML
     1.1 --- a/src/HOL/Integ/IntDiv.ML	Mon Jul 26 16:30:50 1999 +0200
     1.2 +++ b/src/HOL/Integ/IntDiv.ML	Mon Jul 26 16:32:23 1999 +0200
     1.3 @@ -908,7 +908,7 @@
     1.4  by (asm_full_simp_tac (HOL_ss
     1.5  		       addsimps [zmod_zminus_zminus, zdiff_def,
     1.6  				 zminus_zadd_distrib RS sym]) 1);
     1.7 -bd (zminus_equation RS iffD1 RS sym) 1;
     1.8 +by (dtac (zminus_equation RS iffD1 RS sym) 1);
     1.9  by (auto_tac (claset(),
    1.10  	      simpset() addsimps [zmult_zminus_right]));
    1.11  qed "neg_zmod_times_2";
     2.1 --- a/src/HOL/Integ/NatBin.ML	Mon Jul 26 16:30:50 1999 +0200
     2.2 +++ b/src/HOL/Integ/NatBin.ML	Mon Jul 26 16:32:23 1999 +0200
     2.3 @@ -44,7 +44,7 @@
     2.4  (** Successor **)
     2.5  
     2.6  Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
     2.7 -br sym 1;
     2.8 +by (rtac sym 1);
     2.9  by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    2.10  qed "Suc_nat_eq_nat_zadd1";
    2.11