Updated proofs because of new simplification tactics.

--- a/src/HOL/Hoare/List_Examples.ML	Tue Mar 10 19:02:53 1998 +0100
+++ b/src/HOL/Hoare/List_Examples.ML	Tue Mar 10 19:04:10 1998 +0100
@@ -10,7 +10,6 @@
 by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
 by Safe_tac;
 by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
 qed "imperative_reverse";
 
 goal thy
@@ -25,5 +24,4 @@
 by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
 by Safe_tac;
 by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
 qed "imperative_append";

--- a/src/HOL/W0/W.ML	Tue Mar 10 19:02:53 1998 +0100
+++ b/src/HOL/W0/W.ML	Tue Mar 10 19:04:10 1998 +0100
@@ -254,12 +254,8 @@
 by (eres_inst_tac [("x","$ s a")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","m")] allE 1);
-by (dtac asm_rl 1);
-by (dtac asm_rl 1);
-by (dtac asm_rl 1);
 by (Asm_full_simp_tac 1);
 by (safe_tac HOL_cs);
-by (fast_tac HOL_cs 1);
 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
                             conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);