# 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