src/HOL/IMP/Hoare.ML
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
child 5301 e24d15594edd
     1.1 --- a/src/HOL/IMP/Hoare.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/IMP/Hoare.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -56,13 +56,11 @@
     1.4  Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
     1.5  
     1.6  (*Not suitable for rewriting: LOOPS!*)
     1.7 -Goal
     1.8 - "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
     1.9 +Goal "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
    1.10  by (Simp_tac 1);
    1.11  qed "wp_While_if";
    1.12  
    1.13 -Goal
    1.14 -  "wp (WHILE b DO c) Q s = \
    1.15 +Goal "wp (WHILE b DO c) Q s = \
    1.16  \  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
    1.17  by (Simp_tac 1);
    1.18  by (rtac iffI 1);