changeset 290 | 6a6d0bd16035 |
parent 264 | 24199eb2c423 |
child 298 | f2e0d031a395 |
--- a/prio/ExtGG.thy Thu Feb 09 16:34:18 2012 +0000 +++ b/prio/ExtGG.thy Fri Feb 10 11:30:47 2012 +0000 @@ -461,7 +461,7 @@ lemma th_cp_max_preced: "cp (t@s) th = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))" (is "?L = ?R") proof - - have "?L = cpreced (t@s) (wq (t@s)) th" + have "?L = cpreced (wq (t@s)) (t@s) th" by (unfold cp_eq_cpreced, simp) also have "\<dots> = ?R" proof(unfold cpreced_def)