tuned;
authorwenzelm
Thu, 23 Feb 2012 19:34:48 +0100 (2012-02-23)
changeset 46622 3ccecb301d4e
parent 46621 7a8dd77c9f93
child 46623 bce24d3f29e7
tuned;
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