--- a/PrioG.thy~	Fri Dec 18 19:13:19 2015 +0800
+++ b/PrioG.thy~	Fri Dec 18 22:47:32 2015 +0800
@@ -2192,11 +2192,9 @@
   hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) =
                  Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))"
     (is "Max (?f ` ?A) = Max (?f ` ?B)")
-    thm cp_def image_Collect
     unfolding cp_eq_cpreced 
     unfolding cpreced_def .
   obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)"
-    thm Max_in
   proof -
     have h1: "finite (?f ` ?A)"
     proof -
@@ -2231,7 +2229,6 @@
       have "?A \<noteq> {}" by simp
       thus ?thesis by simp
     qed
-    thm Max_in
     from Max_in [OF h1 h2]
     have "Max (?f ` ?A) \<in> (?f ` ?A)" .
     thus ?thesis