# HG changeset patch
# User nipkow
# Date 1008595451 -3600
# Node ID 4ad978c8f5507c9bf8b326e0746e873913430cad
# Parent  66eb843b1d3519643cfb7cbbce5e1d632d5c4a5d
mods due to improved 1-point simprocs (quantifier1).

diff -r 66eb843b1d35 -r 4ad978c8f550 src/HOLCF/IOA/meta_theory/Simulations.ML
--- 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";
 
 
diff -r 66eb843b1d35 -r 4ad978c8f550 src/HOLCF/ex/Focus_ex.ML
--- 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