--- a/CookBook/Readme.thy	Sat Feb 07 14:21:33 2009 +0000
+++ b/CookBook/Readme.thy	Sun Feb 08 08:45:25 2009 +0000
@@ -140,8 +140,6 @@
   @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}
   \end{center}
   
-
-
   \item Functions and value bindings cannot be defined inside antiquotations; they need
   to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
   environments. In this way they are also checked by the compiler. Some \LaTeX-hack in