.

--- a/Slides/Skew_Heap_Slides.thy	Fri Jul 07 14:35:20 2017 +0200
+++ b/Slides/Skew_Heap_Slides.thy	Fri Jul 07 19:24:31 2017 +0200
@@ -115,7 +115,7 @@
   @{term (sub) "log 2 (size1 t1)"} @{text"+"} @{term (sub) "log 2 (size1 t2) + 1"}\\\pause
 @{text"\<le>"} @{term (sub) "log 2 (size1 t1 + size1 t2)"} @{text"+"}
   @{term (sub) "2 * log 2 (size1 t1 + size1 t2) + 1"}\\
-\mbox{}\hfill because @{thm (concl) plus_log_le_2log_plus[where b=2]} if \<open>x,y \<ge> 1\<close>\\\pause
+\mbox{}\hfill because @{thm (concl) plus_log_le_2log_plus[where b=2]} if \<open>x,y > 0\<close>\\\pause
 @{text"="} @{term (sub) "3 * log 2 (size1 t1 + size1 t2) + 1"}
 \end{frame}
 %-------------------------------------------------------------