# HG changeset patch
# User nipkow
# Date 889553050 -3600
# Node ID 3d2375efb80ed09c8e70a15966f542700be394db
# Parent  9e2609b1bfb1241fcd212af95341b29c7433f390
Updated proofs because of new simplification tactics.

diff -r 9e2609b1bfb1 -r 3d2375efb80e src/HOL/Hoare/List_Examples.ML
--- 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";
diff -r 9e2609b1bfb1 -r 3d2375efb80e src/HOL/W0/W.ML
--- 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);