--- a/src/HOL/UNITY/Simple/Common.thy Fri Aug 28 20:18:33 2009 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy Fri Aug 28 20:21:50 2009 +0200
@@ -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 max_def gasc)
+apply (simp add: constrains_def maxfg_def gasc)
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 max_def gasc)
+apply (simp add: constrains_def maxfg_def gasc)
done