# HG changeset patch
# User nipkow
# Date 1251483710 -7200
# Node ID bd13b7756f47a1993effb6a90995e01e5da8321d
# Parent  16464c3f86bd23afd53525ce1961e055bdc0bcb8
tuned proofs

diff -r 16464c3f86bd -r bd13b7756f47 src/HOL/UNITY/Simple/Common.thy
--- 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