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
Tue, 12 May 2009 11:37:40 -0700 fix domain package parsing of lhs sort constraints
huffman [Tue, 12 May 2009 11:37:40 -0700] rev 31161
fix domain package parsing of lhs sort constraints
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip