--- a/src/HOL/IOA/ABP/Correctness.ML Fri Apr 19 11:13:05 1996 +0200
+++ b/src/HOL/IOA/ABP/Correctness.ML Fri Apr 19 11:18:59 1996 +0200
@@ -227,10 +227,6 @@
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);
-(* start states *)
-by (rtac ballI 1);
-by (Simp_tac 1);
(* main-part *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
@@ -243,10 +239,6 @@
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);
- (* start states *)
-by (rtac ballI 1);
-by (Simp_tac 1);
(* main-part *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
@@ -258,10 +250,6 @@
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);
-(* start states *)
-by (rtac ballI 1);
-by (Simp_tac 1);
(* main-part *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);