src/HOL/IMP/Hoare.thy
changeset 20503 503ac4c5ef91
parent 18372 2bffdf62fe7f
child 23746 a455e69c31cc
     1.1 --- a/src/HOL/IMP/Hoare.thy	Mon Sep 11 14:35:30 2006 +0200
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Mon Sep 11 21:35:19 2006 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4  lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
     1.5  
     1.6  lemma wp_is_pre: "|- {wp c Q} c {Q}"
     1.7 -apply (induct c fixing: Q)
     1.8 +apply (induct c arbitrary: Q)
     1.9      apply (simp_all (no_asm))
    1.10      apply fast+
    1.11   apply (blast intro: hoare_conseq1)