fixed problem with back
authorurbanc
Sat, 11 Feb 2012 10:09:39 +0000
changeset 295 8e4a5fff2eda
parent 294 bc5bf9e9ada2
child 296 2c8dcf010567
fixed problem with back
prio/PrioGDef.thy
prio/paper.pdf
--- 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)
 (*>*)
 
Binary file prio/paper.pdf has changed