--- a/thys2/Recs.thy	Wed Jul 24 16:25:03 2013 +0200
+++ b/thys2/Recs.thy	Sat Jul 27 08:14:01 2013 +0200
@@ -569,6 +569,7 @@
 
 section {* Bounded Maximisation *}
 
+
 fun BMax_rec where
   "BMax_rec R 0 = 0"
 | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)"