Updated proofs because of new simplifier.

--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Tue Mar 10 19:04:10 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Tue Mar 10 19:15:00 1998 +0100
@@ -321,7 +321,6 @@
 \         temp_strengthening P2 Q2 h |] \
 \      ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
-auto();
 qed"strength_IMPLIES";
 
 
@@ -335,7 +334,6 @@
 \         temp_weakening P2 Q2 h |] \
 \      ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
-auto();
 qed"weak_AND";
 
 goal thy 
@@ -343,7 +341,6 @@
 \         temp_weakening P2 Q2 h |] \
 \      ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
-auto();
 qed"weak_OR";
 
 goalw thy [temp_strengthening_def]
@@ -358,7 +355,6 @@
 \         temp_weakening P2 Q2 h |] \
 \      ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
-auto();
 qed"weak_IMPLIES";
 
 
@@ -386,12 +382,8 @@
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
 (* UU case *)
-by (clarify_tac set_cs 1);
 by (asm_full_simp_tac (simpset() addsimps [UU_is_Conc])1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
 (* nil case *)
-by (clarify_tac set_cs 1);
 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1);
 (* cons case *)
 by (pair_tac "aa" 1);
@@ -656,4 +648,4 @@
 
 fun abstraction_tac i = 
     SELECT_GOAL (auto_tac (claset() addSIs weak_strength_lemmas,
-                           simpset() addsimps [state_strengthening_def,state_weakening_def])) i;
\ No newline at end of file
+                           simpset() addsimps [state_strengthening_def,state_weakening_def])) i;