Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replaced Best_tac by the one rule needed for the proof
authorpaulson
Wed, 02 Apr 1997 11:30:48 +0200
changeset 2861 7bbd3751523f
parent 2860 6dde30a9e905
child 2862 3f38cbd57d47
Replaced Best_tac by the one rule needed for the proof
src/HOL/IMP/Hoare.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle