src/HOL/IMP/Hoare.thy
changeset 13630 a013a9dd370f
parent 12546 0c90e581379f
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/IMP/Hoare.thy	Mon Oct 07 19:01:51 2002 +0200
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Tue Oct 08 08:20:17 2002 +0200
     1.3 @@ -116,9 +116,7 @@
     1.4   apply (rule weak_coinduct)
     1.5    apply (erule CollectI)
     1.6   apply safe
     1.7 -  apply (rotate_tac -1)
     1.8    apply simp
     1.9 - apply (rotate_tac -1)
    1.10   apply simp
    1.11  apply (simp add: wp_def Gamma_def)
    1.12  apply (intro strip)
    1.13 @@ -146,8 +144,8 @@
    1.14   apply (rule hoare_conseq1)
    1.15    prefer 2 apply (fast)
    1.16    apply safe
    1.17 - apply (rotate_tac -1, simp)
    1.18 -apply (rotate_tac -1, simp)
    1.19 + apply simp
    1.20 +apply simp
    1.21  done
    1.22  
    1.23  lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"