# 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) \ {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 {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