mods due to improved 1-point simprocs (quantifier1).

--- a/src/HOLCF/IOA/meta_theory/Simulations.ML	Mon Dec 17 14:23:10 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.ML	Mon Dec 17 14:24:11 2001 +0100
@@ -28,10 +28,7 @@
 
 Goalw [is_ref_map_def,is_simulation_def]
 "!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A";
-(* start states *)
 by (Asm_full_simp_tac 1);
-(* main case *)
-by (Blast_tac 1);
 qed"ref_map_is_simulation";
 
 

--- a/src/HOLCF/ex/Focus_ex.ML	Mon Dec 17 14:23:10 2001 +0100
+++ b/src/HOLCF/ex/Focus_ex.ML	Mon Dec 17 14:24:11 2001 +0100
@@ -1,4 +1,3 @@
-
 (* first some logical trading *)
 
 val prems = goal Focus_ex.thy
@@ -128,12 +127,6 @@
 \ -->\
 \ (? g. def_g(g::'b stream -> 'c stream ))";
 by (simp_tac (HOL_ss addsimps [def_g]) 1);
-by (strip_tac 1);
-by (etac exE 1);
-by (rtac exI 1);
-by (rtac exI 1);
-by (etac conjI 1);
-by (rtac refl 1);
 val L2 = result();
 
 val prems = goal Focus_ex.thy