# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1354808960 0
# Node ID 51019d035a7945f3f57f3bb882615a06a8f7fc22
# Parent  a04084de4946144aba278765d721e9338affd641
made everything working

diff -r a04084de4946 -r 51019d035a79 PrioG.thy
--- 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
diff -r a04084de4946 -r 51019d035a79 Slides/Slides1.thy
--- 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}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
diff -r a04084de4946 -r 51019d035a79 Slides/document/EventAbstract.png
Binary file Slides/document/EventAbstract.png has changed
diff -r a04084de4946 -r 51019d035a79 Slides/document/PriorityInversion.png
Binary file Slides/document/PriorityInversion.png has changed
diff -r a04084de4946 -r 51019d035a79 Slides/document/marspath1.png
Binary file Slides/document/marspath1.png has changed
diff -r a04084de4946 -r 51019d035a79 Slides/document/marspath3.png
Binary file Slides/document/marspath3.png has changed
diff -r a04084de4946 -r 51019d035a79 Slides/document/marsrover.png
Binary file Slides/document/marsrover.png has changed