# HG changeset patch
# User zhang
# Date 1329059570 0
# Node ID d9b0a2fd0db7c0819ad7420234e4f31c818806cb
# Parent  06241c45cb17229d714386fda8ed1a203df1ebb2
Correct a mistake.

diff -r 06241c45cb17 -r d9b0a2fd0db7 prio/ExtGG.thy
--- a/prio/ExtGG.thy	Sun Feb 12 15:05:57 2012 +0000
+++ b/prio/ExtGG.thy	Sun Feb 12 15:12:50 2012 +0000
@@ -895,7 +895,7 @@
 lemma runing_inversion_3:
   assumes runing': "th' \<in> runing (t@s)"
   and neq_th: "th' \<noteq> th"
-  shows "(th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"
+  shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"
 proof -
   from runing_inversion_2 [OF runing'] and neq_th
   show ?thesis by auto