--- a/src/HOL/Sum.ML Wed Apr 09 12:31:11 1997 +0200
+++ b/src/HOL/Sum.ML Wed Apr 09 12:32:04 1997 +0200
@@ -185,7 +185,7 @@
qed "Part_subset";
goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_mono";
val basic_monos = basic_monos @ [Part_mono];
@@ -199,10 +199,10 @@
qed "Part_id";
goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_Int";
(*For inductive definitions*)
goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_Collect";