src/HOL/IMP/VC.thy
changeset 20503 503ac4c5ef91
parent 18372 2bffdf62fe7f
child 23746 a455e69c31cc
     1.1 --- a/src/HOL/IMP/VC.thy	Mon Sep 11 14:35:30 2006 +0200
     1.2 +++ b/src/HOL/IMP/VC.thy	Mon Sep 11 21:35:19 2006 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  lemma l: "!s. P s --> P s" by fast
     1.5  
     1.6  lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip 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 fast
    1.12 @@ -151,6 +151,6 @@
    1.13  qed
    1.14  
    1.15  lemma vcawp_vc_awp: "vcawp c Q = (vc c Q, awp c Q)"
    1.16 -  by (induct c fixing: Q) (simp_all add: Let_def)
    1.17 +  by (induct c arbitrary: Q) (simp_all add: Let_def)
    1.18  
    1.19  end