# HG changeset patch
# User lcp
# Date 797851413 -7200
# Node ID c3913a79b6aeab0bf4db79cfb76b0317d8dd17df
# Parent  05736fb55c13ecaaebc77f8a5545eb589c236c30
Simplified some proofs and made them work for new hyp_subst_tac.

diff -r 05736fb55c13 -r c3913a79b6ae ex/MT.ML
--- 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);