--- a/PrioG.thy	Thu Dec 06 15:12:49 2012 +0000
+++ b/PrioG.thy	Thu Dec 06 15:49:20 2012 +0000
@@ -1033,7 +1033,8 @@
           show ?thesis by (unfold h, simp)
         next
           assume "\<exists> a. ?D = {a}"
-          thus ?thesis by auto
+          thus ?thesis
+            by (metis finite.simps)
         qed
       qed
       ultimately show ?thesis by simp

--- a/Slides/Slides1.thy	Thu Dec 06 15:12:49 2012 +0000
+++ b/Slides/Slides1.thy	Thu Dec 06 15:49:20 2012 +0000
@@ -349,9 +349,9 @@
 
   \pause
 
-  \begin{center}
-  \includegraphics[scale=0.4]{EventAbstract.png}
-  \end{center}
+%  \begin{center}
+%  \includegraphics[scale=0.4]{EventAbstract.png}
+%  \end{center}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

Binary file Slides/document/EventAbstract.png has changed

Binary file Slides/document/PriorityInversion.png has changed

Binary file Slides/document/marspath1.png has changed

Binary file Slides/document/marspath3.png has changed

Binary file Slides/document/marsrover.png has changed