--- a/prio/ExtGG.thy	Tue Jan 24 00:34:52 2012 +0000
+++ b/prio/ExtGG.thy	Fri Jan 27 13:50:02 2012 +0000
@@ -32,7 +32,6 @@
   assumes vt_s: "vt step s"
   and threads_s: "th \<in> threads s"
   and highest: "preced th s = Max ((cp s)`threads s)"
-  and nh: "preced th s' \<noteq> Max ((cp s)`threads s')"
   and preced_th: "preced th s = Prc prio tm"
 
 context highest_gen
@@ -119,8 +118,6 @@
 context extend_highest_gen
 begin
 
-thm extend_highest_gen.axioms
-
 lemma red_moment:
   "extend_highest_gen s th prio tm (moment i t)"
   apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
@@ -164,7 +161,7 @@
 qed
 
 lemma th_kept: "th \<in> threads (t @ s) \<and> 
-        preced th (t@s) = preced th s" (is "?Q t")
+                 preced th (t@s) = preced th s" (is "?Q t")
 proof -
   show ?thesis
   proof(induct rule:ind)
@@ -521,7 +518,7 @@
 lemma th_cp_preced: "cp (t@s) th = preced th s"
   by (fold max_kept, unfold th_cp_max_preced, simp)
 
-lemma preced_less':
+lemma preced_less:
   fixes th'
   assumes th'_in: "th' \<in> threads s"
   and neq_th': "th' \<noteq> th"