# 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