--- a/Implementation.thy	Tue Jun 14 15:06:16 2016 +0100
+++ b/Implementation.thy	Fri Jun 17 09:46:25 2016 +0100
@@ -154,7 +154,7 @@
 proof -
  from holding_th_cs_s
  show ?thesis 
-    by (unfold s_RAG_def holding_eq, auto)
+    by (unfold s_RAG_def s_holding_abv, auto)
 qed
 
 lemma ancestors_cs: 
@@ -187,7 +187,7 @@
 lemma sub_RAGs': 
   "{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s"
   using waiting_taker holding_th_cs_s
-  by (unfold s_RAG_def, fold waiting_eq holding_eq, auto)
+  by (unfold s_RAG_def, fold s_waiting_abv s_holding_abv, auto)
 
 lemma ancestors_th': 
   "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" 
@@ -297,7 +297,7 @@
         by (auto simp:ancestors_def)
       from tranclD2[OF this]
       obtain th' where "waiting s th' cs"
-        by (auto simp:s_RAG_def waiting_eq)
+        by (auto simp:s_RAG_def s_waiting_abv)
       with no_waiter_before 
       show ?thesis by simp
     qed simp
@@ -390,7 +390,7 @@
 
 lemma cs_held: "(Cs cs, Th holder) \<in> RAG s"
   using holding_s_holder
-  by (unfold s_RAG_def, fold holding_eq, auto)
+  by (unfold s_RAG_def, fold s_holding_abv, auto)
 
 lemma tRAG_s: 
   "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"
@@ -662,7 +662,7 @@
     assume "Th th \<in> Range (RAG s)"
     then obtain cs where "holding s th cs"
     by (simp add: holdents_RAG holdents_th_s)
-    then show False by (unfold holding_eq, auto)
+    then show False by (unfold s_holding_abv, auto)
   qed
   moreover have "Th th \<notin> Domain (RAG s)"
   proof