# HG changeset patch
# User urbanc
# Date 1328954979 0
# Node ID 8e4a5fff2eda2c672e4cdd481744c22eb4f3f918
# Parent  bc5bf9e9ada2c72728c6d0a1ea39640377ccbeea
fixed problem with back

diff -r bc5bf9e9ada2 -r 8e4a5fff2eda prio/PrioGDef.thy
--- a/prio/PrioGDef.thy	Sat Feb 11 09:34:46 2012 +0000
+++ b/prio/PrioGDef.thy	Sat Feb 11 10:09:39 2012 +0000
@@ -198,8 +198,7 @@
   "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})"
   unfolding cpreced_def image_def
   apply(rule eq_reflection)
-  apply(rule arg_cong)
-  back
+  apply(rule_tac f="Max" in arg_cong)
   by (auto)
 (*>*)
 
diff -r bc5bf9e9ada2 -r 8e4a5fff2eda prio/paper.pdf
Binary file prio/paper.pdf has changed