| changeset 7127 | 48e235179ffb |
| parent 6162 | 484adda70b65 |
| child 8573 | fc22f59f5ae7 |
--- a/src/HOL/Hoare/Hoare.ML Wed Jul 28 22:01:58 1999 +0200 +++ b/src/HOL/Hoare/Hoare.ML Thu Jul 29 12:44:57 1999 +0200 @@ -38,7 +38,7 @@ val lemma = result() RS spec RS spec RS mp RS mp; Goalw [Valid_def] - "[| p <= i; Valid (i Int b) c i; (i Int -b) <= q |] \ + "[| p <= i; Valid (i Int b) c i; i Int (-b) <= q |] \ \ ==> Valid p (WHILE b INV {i} DO c OD) q"; by (Asm_simp_tac 1); by (Clarify_tac 1);