# HG changeset patch
# User clasohm
# Date 829905539 -7200
# Node ID 6056e9c967d9ea61ea36eaaeaa70661df543801d
# Parent  5183de4c496dfbe83cf3d0ac1aa58a0363c8de13
adapted to new version of Fun.ML

diff -r 5183de4c496d -r 6056e9c967d9 src/HOL/IOA/ABP/Correctness.ML
--- 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);
diff -r 5183de4c496d -r 6056e9c967d9 src/HOL/IOA/meta_theory/Solve.ML
--- a/src/HOL/IOA/meta_theory/Solve.ML	Fri Apr 19 11:13:05 1996 +0200
+++ b/src/HOL/IOA/meta_theory/Solve.ML	Fri Apr 19 11:18:59 1996 +0200
@@ -223,7 +223,6 @@
 by (asm_full_simp_tac (!simpset addsimps [is_weak_pmap_def]) 1);
 by (rtac conjI 1);
 by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1);
-by (fast_tac set_cs 1);
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
 by (simp_tac (!simpset addsimps [rename_def]) 1);
@@ -265,6 +264,3 @@
 by (eres_inst_tac [("x","x")] allE 1);
 by (Asm_full_simp_tac 1);
 qed"rename_through_pmap";
-
-
-