2009-05-16 merged
nipkow [Sat, 16 May 2009 11:28:23 +0200] rev 31167
merged
2009-05-16 "{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".
2009-05-15 merged
huffman [Fri, 15 May 2009 15:13:09 -0700] rev 31165
merged
2009-05-15 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
2009-05-12 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
2009-05-12 add cpo_type function
huffman [Tue, 12 May 2009 12:01:25 -0700] rev 31162
add cpo_type function
2009-05-12 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
2009-05-12 export quiet_mode and trace_domain refs for domain package
huffman [Tue, 12 May 2009 10:40:09 -0700] rev 31160
export quiet_mode and trace_domain refs for domain package
2009-05-15 new lemma
nipkow [Fri, 15 May 2009 10:01:57 +0200] rev 31159
new lemma
2009-05-14 merged
haftmann [Thu, 14 May 2009 21:57:03 +0200] rev 31158
merged
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip