# HG changeset patch
# User oheimb
# Date 833564843 -7200
# Node ID 6c942cf3bf68ddc2954c022ea349c752d105d33d
# Parent  47c47b7d7aa8bb48637f83f9f7225fad5a7635aa
adapted some proofs for new simplifier

diff -r 47c47b7d7aa8 -r 6c942cf3bf68 src/HOL/IOA/ABP/Correctness.ML
--- a/src/HOL/IOA/ABP/Correctness.ML	Fri May 31 19:34:40 1996 +0200
+++ b/src/HOL/IOA/ABP/Correctness.ML	Fri May 31 19:47:23 1996 +0200
@@ -227,9 +227,10 @@
 goal Correctness.thy 
       "is_weak_pmap (%id.id) sender_ioa sender_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-by (rtac conjI 1);
+by (TRY(
+   (rtac conjI 1) THEN
 (* start states *)
-by (fast_tac set_cs 1);
+   (fast_tac set_cs 1)));
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
@@ -242,9 +243,10 @@
 goal Correctness.thy 
       "is_weak_pmap (%id.id) receiver_ioa receiver_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-by (rtac conjI 1);
+by (TRY(
+   (rtac conjI 1) THEN
  (* start states *)
-by (fast_tac set_cs 1);
+   (fast_tac set_cs 1)));
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
@@ -256,9 +258,10 @@
 goal Correctness.thy 
       "is_weak_pmap (%id.id) env_ioa env_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-by (rtac conjI 1);
+by (TRY(
+   (rtac conjI 1) THEN
 (* start states *)
-by (fast_tac set_cs 1);
+   (fast_tac set_cs 1)));
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);