author | wenzelm |
Thu, 23 Feb 2012 19:34:48 +0100 (2012-02-23) | |
changeset 46622 | 3ccecb301d4e |
parent 46621 | 7a8dd77c9f93 |
child 46623 | bce24d3f29e7 |
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Thu Feb 23 18:38:30 2012 +0100 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Thu Feb 23 19:34:48 2012 +0100 @@ -249,9 +249,9 @@ by hoare auto -subsection{* Time *} +subsection {* Time *} -text{* A simple embedding of time in Hoare logic: function @{text +text {* A simple embedding of time in Hoare logic: function @{text timeit} inserts an extra variable to keep track of the elapsed time. *} record tstate = time :: nat