# HG changeset patch
# User paulson
# Date 834747902 -7200
# Node ID c055505f36d1d2aff0885bf9399fba3c5e290557
# Parent  334308d2afbce160a9fd326d8431d2475042252c
Explicitly included add_mult_distrib & add_mult_distrib2

diff -r 334308d2afbc -r c055505f36d1 src/HOL/Hoare/Examples.ML
--- 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";
diff -r 334308d2afbc -r c055505f36d1 src/HOL/Integ/Integ.ML
--- 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;