src/HOL/IMP/VC.thy
changeset 12434 ff2efde4574d
parent 12431 07ec657249e5
child 13596 ee5f79b210c1
     1.1 --- a/src/HOL/IMP/VC.thy	Sun Dec 09 14:37:42 2001 +0100
     1.2 +++ b/src/HOL/IMP/VC.thy	Sun Dec 09 15:26:13 2001 +0100
     1.3 @@ -90,7 +90,8 @@
     1.4  apply fast
     1.5  done
     1.6  
     1.7 -lemma awp_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
     1.8 +lemma awp_mono [rule_format (no_asm)]: 
     1.9 +  "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
    1.10  apply (induct_tac "c")
    1.11      apply (simp_all (no_asm_simp))
    1.12  apply (rule allI, rule allI, rule impI)
    1.13 @@ -99,7 +100,8 @@
    1.14  done
    1.15  
    1.16  
    1.17 -lemma vc_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
    1.18 +lemma vc_mono [rule_format (no_asm)]: 
    1.19 +  "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
    1.20  apply (induct_tac "c")
    1.21      apply (simp_all (no_asm_simp))
    1.22  apply safe