Explicitly included add_mult_distrib & add_mult_distrib2

--- a/src/HOL/Hoare/Examples.ML	Fri Jun 14 12:23:31 1996 +0200
+++ b/src/HOL/Hoare/Examples.ML	Fri Jun 14 12:25:02 1996 +0200
@@ -110,11 +110,11 @@
 \ {b = fac A}";
 
 by (hoare_tac 1);
-
 by (safe_tac HOL_cs);
-
 by (res_inst_tac [("n","a")] natE 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [mult_assoc])));
+by (ALLGOALS
+    (asm_simp_tac
+     (!simpset addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
 by (fast_tac HOL_cs 1);
 
 qed"factorial";

--- a/src/HOL/Integ/Integ.ML	Fri Jun 14 12:23:31 1996 +0200
+++ b/src/HOL/Integ/Integ.ML	Fri Jun 14 12:25:02 1996 +0200
@@ -342,8 +342,7 @@
 by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
 by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
 by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
-by (asm_simp_tac (!simpset delsimps [add_mult_distrib]
-                           addsimps [add_mult_distrib RS sym]) 1);
+by (asm_simp_tac (!simpset addsimps [add_mult_distrib RS sym]) 1);
 by (asm_simp_tac (!simpset addsimps add_ac@mult_ac) 1);
 qed "zmult_congruent2";
 
@@ -397,7 +396,8 @@
 by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
-by (asm_simp_tac (!simpset addsimps ([zmult] @ add_ac @ mult_ac)) 1);
+by (asm_simp_tac (!simpset addsimps ([add_mult_distrib2,zmult] @ 
+				     add_ac @ mult_ac)) 1);
 qed "zmult_assoc";
 
 (*For AC rewriting*)
@@ -414,7 +414,8 @@
 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (asm_simp_tac 
-    (!simpset addsimps ([zadd, zmult] @ add_ac @ mult_ac)) 1);
+    (!simpset addsimps ([add_mult_distrib2, zadd, zmult] @ 
+			add_ac @ mult_ac)) 1);
 qed "zadd_zmult_distrib";
 
 val zmult_commute'= read_instantiate [("z","w")] zmult_commute;