isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

Sat, 16 May 2009 10:19:01 +0200 merged

bulwahn [Sat, 16 May 2009 10:19:01 +0200] rev 31171

merged

Fri, 15 May 2009 15:56:28 +0200 added predicate transformation function for code generation

bulwahn [Fri, 15 May 2009 15:56:28 +0200] rev 31170

added predicate transformation function for code generation

Fri, 15 May 2009 15:29:34 +0200 added predicate transformation function for code generation

bulwahn [Fri, 15 May 2009 15:29:34 +0200] rev 31169

added predicate transformation function for code generation

Sat, 16 May 2009 17:44:11 +0200 proof tuned

nipkow [Sat, 16 May 2009 17:44:11 +0200] rev 31168

proof tuned

Sat, 16 May 2009 11:28:23 +0200 merged

nipkow [Sat, 16 May 2009 11:28:23 +0200] rev 31167

merged

Sat, 16 May 2009 11:28:02 +0200 "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"

nipkow [Sat, 16 May 2009 11:28:02 +0200] rev 31166

"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".

Fri, 15 May 2009 15:13:09 -0700 merged

huffman [Fri, 15 May 2009 15:13:09 -0700] rev 31165

merged

Fri, 15 May 2009 15:12:23 -0700 continuity proofs for approx function on deflations; lemma cast_below_imp_below

huffman [Fri, 15 May 2009 15:12:23 -0700] rev 31164

continuity proofs for approx function on deflations; lemma cast_below_imp_below

Tue, 12 May 2009 12:16:33 -0700 allow lazy domain arguments to have class cpo

huffman [Tue, 12 May 2009 12:16:33 -0700] rev 31163

allow lazy domain arguments to have class cpo

Tue, 12 May 2009 12:01:25 -0700 add cpo_type function

huffman [Tue, 12 May 2009 12:01:25 -0700] rev 31162

add cpo_type function

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle