--- a/Test.thy	Wed Sep 09 11:24:19 2015 +0100
+++ b/Test.thy	Sun Oct 04 23:02:57 2015 +0100
@@ -6,6 +6,8 @@
 type_synonym priority = nat  -- {* Type for priorities. *}
 type_synonym cs = nat -- {* Type for critical sections (or resources). *}
 
+-- {* Schedulling Events *}
+
 datatype event = 
   Create thread priority 
 | Exit thread 
@@ -36,6 +38,7 @@
 | "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)" 
 | "last_set th (_#s) = last_set th s"
 
+
 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
   where "preced th s \<equiv> Prc (priority th s) (last_set th s)"
 
@@ -48,6 +51,7 @@
 definition
   "waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)"
 
+--{* Nodes in Resource Graph *}
 datatype node = 
   Th "thread" 
 | Cs "cs" 
@@ -83,9 +87,9 @@
 
 lemma [simp]: 
   "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)"
-apply(auto)
-apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
-by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
+apply(rule iffI)
+apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)+
+done
 
 abbreviation
   "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"