Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IMP/Hoare.thy
changeset 13630 a013a9dd370f
parent 12546 0c90e581379f
child 16417 9bc16273c2d4 
--- a/src/HOL/IMP/Hoare.thy	Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/IMP/Hoare.thy	Tue Oct 08 08:20:17 2002 +0200
@@ -116,9 +116,7 @@
  apply (rule weak_coinduct)
   apply (erule CollectI)
  apply safe
-  apply (rotate_tac -1)
   apply simp
- apply (rotate_tac -1)
  apply simp
 apply (simp add: wp_def Gamma_def)
 apply (intro strip)
@@ -146,8 +144,8 @@
  apply (rule hoare_conseq1)
   prefer 2 apply (fast)
   apply safe
- apply (rotate_tac -1, simp)
-apply (rotate_tac -1, simp)
+ apply simp
+apply simp
 done
 
 lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"
isabelle