| changeset 58410 | 6d46ad54a2ab |
| parent 54489 | 03ff4d1e6784 |
| child 61028 | 99d58362eeeb |
--- a/src/HOL/IMP/Hoare_Examples.thy Sun Sep 21 16:56:06 2014 +0200 +++ b/src/HOL/IMP/Hoare_Examples.thy Sun Sep 21 16:56:11 2014 +0200 @@ -17,7 +17,7 @@ abbreviation "wsum == WHILE Less (N 0) (V ''x'') DO (''y'' ::= Plus (V ''y'') (V ''x'');; - ''x'' ::= Plus (V ''x'') (N -1))" + ''x'' ::= Plus (V ''x'') (N (- 1)))" subsubsection{* Proof by Operational Semantics *}