# HG changeset patch
# User paulson
# Date 859973448 -7200
# Node ID 7bbd3751523fb42a03143ce6757a79f9f50cf2e5
# Parent  6dde30a9e905db8561072f05a16ddec062879f64
Replaced Best_tac by the one rule needed for the proof

diff -r 6dde30a9e905 -r 7bbd3751523f src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Wed Apr 02 11:30:03 1997 +0200
+++ b/src/HOL/IMP/Hoare.ML	Wed Apr 02 11:30:48 1997 +0200
@@ -70,7 +70,7 @@
 by(simp_tac (!simpset setloop(split_tac[expand_if])) 1);
 br iffI 1;
  br weak_coinduct 1;
-  by(Best_tac 1);
+  by(etac CollectI 1);
  by(safe_tac (!claset));
   by(rotate_tac ~1 1);
   by(Asm_full_simp_tac 1);