nipkow [Sat, 16 May 2009 11:28:23 +0200] rev 31167
merged
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".
huffman [Fri, 15 May 2009 15:13:09 -0700] rev 31165
merged
huffman [Fri, 15 May 2009 15:12:23 -0700] rev 31164
continuity proofs for approx function on deflations; lemma cast_below_imp_below
huffman [Tue, 12 May 2009 12:16:33 -0700] rev 31163
allow lazy domain arguments to have class cpo
huffman [Tue, 12 May 2009 12:01:25 -0700] rev 31162
add cpo_type function
huffman [Tue, 12 May 2009 11:37:40 -0700] rev 31161
fix domain package parsing of lhs sort constraints
huffman [Tue, 12 May 2009 10:40:09 -0700] rev 31160
export quiet_mode and trace_domain refs for domain package
nipkow [Fri, 15 May 2009 10:01:57 +0200] rev 31159
new lemma
haftmann [Thu, 14 May 2009 21:57:03 +0200] rev 31158
merged