| changeset 72806 | 4fa08e083865 |
| parent 69597 | ff784d5a5bfb |
| child 72990 | db8f94656024 |
--- a/src/HOL/Hoare/SchorrWaite.thy Fri Dec 04 13:24:49 2020 +0100 +++ b/src/HOL/Hoare/SchorrWaite.thy Fri Dec 04 15:07:47 2020 +0100 @@ -222,7 +222,7 @@ (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}") proof (vcg) let "While {(c, m, l, r, t, p, q, root). ?whileB m t p} - {(c, m, l, r, t, p, q, root). ?inv c m l r t p} ?body" = ?c3 + {(c, m, l, r, t, p, q, root). ?inv c m l r t p} _ ?body" = ?c3 { fix c m l r t p q root