--- a/PIPDefs.thy	Wed Aug 24 16:13:20 2016 +0200
+++ b/PIPDefs.thy	Sun Oct 02 14:32:05 2016 +0100
@@ -125,7 +125,7 @@
 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
   where "preced th s \<equiv> Prc (priority th s) (last_set th s)"
 
-definition preceds :: "thread set \<Rightarrow> state \<Rightarrow> precedence set"
+abbreviation preceds :: "thread set \<Rightarrow> state \<Rightarrow> precedence set"
   where "preceds ths s \<equiv> {preced th s | th. th \<in> ths}"
 
 text {*
@@ -227,7 +227,7 @@
 
 lemma cpreced_def2:
   "cpreced wq s th \<equiv> Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th))"
-  unfolding cpreced_def image_def preceds_def
+  unfolding cpreced_def image_def
   apply(rule eq_reflection)
   apply(rule_tac f="Max" in arg_cong)
   by (auto)
@@ -379,7 +379,7 @@
 apply(rule ext)
 apply(simp add: cpreced_def)
 apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def)
-apply(simp add: preced_def preceds_def)
+apply(simp add: preced_def)
 done
 
 text {*