# HG changeset patch
# User paulson
# Date 844678021 -7200
# Node ID 2395bc55b3e690b3af476e7f63ef58b4c54d7e59
# Parent  8d4558d95e9a58f27916df37abac14cff2dcade5
New proof required by change to simpdata.ML

diff -r 8d4558d95e9a -r 2395bc55b3e6 src/HOL/IOA/meta_theory/Solve.ML
--- a/src/HOL/IOA/meta_theory/Solve.ML	Mon Oct 07 10:43:40 1996 +0200
+++ b/src/HOL/IOA/meta_theory/Solve.ML	Mon Oct 07 10:47:01 1996 +0200
@@ -79,9 +79,6 @@
       (!simpset addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
                 setloop (split_tac[expand_if,expand_option_case])) 1);
- by (strip_tac 1);
- by (REPEAT(hyp_subst_tac 1)); 
- by (Asm_full_simp_tac 1);
 qed"comp1_reachable";
 
 
@@ -102,9 +99,6 @@
       (!simpset addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
                 setloop (split_tac[expand_if,expand_option_case])) 1);
- by (strip_tac 1);
- by (REPEAT(hyp_subst_tac 1)); 
- by (Asm_full_simp_tac 1);
 qed"comp2_reachable";
 
 
@@ -168,7 +162,7 @@
       (!simpset addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,rename_def]
                 setloop (split_tac[expand_option_case])) 1);
-by(Auto_tac());
+by (best_tac (!claset addSDs [spec] addDs [sym] addss (!simpset)) 1);
 qed"reachable_rename_ioa";