diff -r b9d0dd18c81e -r f2bda6ba4952 thys/turing_hoare.thy
--- a/thys/turing_hoare.thy	Sun Jan 27 20:01:13 2013 +0000
+++ b/thys/turing_hoare.thy	Mon Jan 28 02:38:57 2013 +0000
@@ -29,10 +29,11 @@
 
 (* halting case *)
 definition
-  Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" [50, 49] 50)
+  Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
 where
   "{P} p {Q} \<equiv> \<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n))"
 
+
 (* not halting case *)
 definition
   Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50)