--- a/PrioG.thy	Fri May 30 07:56:39 2014 +0100
+++ b/PrioG.thy	Mon Jun 02 14:58:42 2014 +0100
@@ -804,19 +804,6 @@
   apply(auto)
   done
 
-(* FIXME: Unused
-lemma simple_A:
-  fixes A
-  assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"
-  shows "A = {} \<or> (\<exists> a. A = {a})"
-proof(cases "A = {}")
-  case True thus ?thesis by simp
-next
-  case False then obtain a where "a \<in> A" by auto
-  with h have "A = {a}" by auto
-  thus ?thesis by simp
-qed
-*)
 
 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
   by (unfold s_RAG_def, auto)
@@ -2092,7 +2079,7 @@
 apply(simp add: Let_def)
 done
 
-
+(* FIXME: NOT NEEDED *)
 lemma runing_unique:
   fixes th1 th2 s
   assumes vt: "vt s"
@@ -2281,6 +2268,7 @@
   qed
 qed
 
+
 lemma create_pre:
   assumes stp: "step s e"
   and not_in: "th \<notin> threads s"