# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1374905641 -7200
# Node ID 00ac265b251bb723019fc81ff7e591cff74bf8b0
# Parent  19a4ac992823bd9bd37d1a62b52ddb107da1f48c
updated

diff -r 19a4ac992823 -r 00ac265b251b slides2.pdf
Binary file slides2.pdf has changed
diff -r 19a4ac992823 -r 00ac265b251b thys2/Recs.thy
--- 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)"