# HG changeset patch
# User nipkow
# Date 840798771 -7200
# Node ID 9bd1c8826f5c6d487c230833cea0df635fd4077c
# Parent  ad5bb12605fbdf66f4c7f507ac600d61df8b1ea3
Swaped two conditions in the completeness statement.

diff -r ad5bb12605fb -r 9bd1c8826f5c 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);