src/HOL/IMP/VC.ML

--- a/src/HOL/IMP/VC.ML	Fri Aug 23 13:03:02 1996 +0200
+++ b/src/HOL/IMP/VC.ML	Fri Aug 23 13:12:51 1996 +0200
@@ -56,7 +56,7 @@
 
 goal VC.thy
   "!!P c Q. |- {P}c{Q} ==> \
-\          (? ac. astrip ac = c & (!s. P s --> wp ac Q s) & (!s. vc ac Q s))";
+\          (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> wp ac Q s))";
 by (etac hoare.induct 1);
      by(res_inst_tac [("x","Askip")] exI 1);
      by(Simp_tac 1);