src/HOL/IMP/VC.ML
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
     1.1 --- a/src/HOL/IMP/VC.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/IMP/VC.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -43,8 +43,7 @@
     1.4  by (fast_tac (HOL_cs addEs [awp_mono]) 1);
     1.5  qed_spec_mp "vc_mono";
     1.6  
     1.7 -Goal
     1.8 -  "|- {P}c{Q} ==> \
     1.9 +Goal "|- {P}c{Q} ==> \
    1.10  \  (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
    1.11  by (etac hoare.induct 1);
    1.12       by (res_inst_tac [("x","Askip")] exI 1);