# HG changeset patch # User wenzelm # Date 1330022088 -3600 # Node ID 3ccecb301d4e23e9d9b5c621edec5ebfca58aa5e # Parent 7a8dd77c9f931a48df2360b7bf4b42740ab770bb tuned; diff -r 7a8dd77c9f93 -r 3ccecb301d4e src/HOL/Isar_Examples/Hoare_Ex.thy --- 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