equal
deleted
inserted
replaced
247 OD |
247 OD |
248 .{\<acute>S = (SUM j<n. j)}." |
248 .{\<acute>S = (SUM j<n. j)}." |
249 by hoare auto |
249 by hoare auto |
250 |
250 |
251 |
251 |
252 subsection{* Time *} |
252 subsection {* Time *} |
253 |
253 |
254 text{* A simple embedding of time in Hoare logic: function @{text |
254 text {* A simple embedding of time in Hoare logic: function @{text |
255 timeit} inserts an extra variable to keep track of the elapsed time. *} |
255 timeit} inserts an extra variable to keep track of the elapsed time. *} |
256 |
256 |
257 record tstate = time :: nat |
257 record tstate = time :: nat |
258 |
258 |
259 type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>" |
259 type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>" |