--- a/src/HOL/UNITY/Simple/Common.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/UNITY/Simple/Common.thy Wed Dec 25 17:39:06 2013 +0100
@@ -65,7 +65,7 @@
lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
\<in> {m} co (maxfg m)"
apply (simp add: mk_total_program_def)
-apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
+apply (simp add: constrains_def maxfg_def gasc max.absorb2)
done
(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
@@ -73,7 +73,7 @@
(UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)
\<in> {m} co (maxfg m)"
apply (simp add: mk_total_program_def)
-apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
+apply (simp add: constrains_def maxfg_def gasc max.absorb2)
done