--- a/ex/MT.ML Thu Apr 06 11:52:05 1995 +0200
+++ b/ex/MT.ML Fri Apr 14 11:23:33 1995 +0200
@@ -39,16 +39,11 @@
);
val prems = goal MT.thy "P(a,b) ==> P(fst(<a,b>),snd(<a,b>))";
-by (rtac (fst_conv RS ssubst) 1);
-by (rtac (snd_conv RS ssubst) 1);
-by (resolve_tac prems 1);
+by (simp_tac (prod_ss addsimps prems) 1);
qed "infsys_p1";
-val prems = goal MT.thy "P(fst(<a,b>),snd(<a,b>)) ==> P(a,b)";
-by (cut_facts_tac prems 1);
-by (dtac (fst_conv RS subst) 1);
-by (dtac (snd_conv RS subst) 1);
-by (assume_tac 1);
+val prems = goal MT.thy "!!a b. P(fst(<a,b>),snd(<a,b>)) ==> P(a,b)";
+by (asm_full_simp_tac prod_ss 1);
qed "infsys_p2";
val prems = goal MT.thy
@@ -649,10 +644,9 @@
(* The pointwise extension of hasty to environments *)
(* ############################################################ *)
-val prems = goal MT.thy
- "[| ve hastyenv te; v hasty t |] ==> \
-\ ve + {ev |-> v} hastyenv te + {ev |=> t}";
-by (cut_facts_tac prems 1);
+goal MT.thy
+ "!!ve. [| ve hastyenv te; v hasty t |] ==> \
+\ ve + {ev |-> v} hastyenv te + {ev |=> t}";
by (rewtac hasty_env_def);
by (asm_full_simp_tac (HOL_ss addsimps [ve_dom_owr, te_dom_owr]) 1);
by (safe_tac HOL_cs);