krauss [Sun, 12 Dec 2010 21:41:01 +0100] rev 41114
tuned headers
krauss [Sun, 12 Dec 2010 21:40:59 +0100] rev 41113
added signature;
more honest header
huffman [Sat, 11 Dec 2010 21:27:53 -0800] rev 41112
add HOLCF library theories with cpo/predomain instances for HOL types
huffman [Sat, 11 Dec 2010 11:26:37 -0800] rev 41111
xsymbol notation for powerdomain types
huffman [Sat, 11 Dec 2010 10:35:40 -0800] rev 41110
new powerdomain lemmas
krauss [Sat, 11 Dec 2010 00:14:12 +0100] rev 41109
made smlnj happy
haftmann [Fri, 10 Dec 2010 16:10:57 +0100] rev 41108
merged
haftmann [Fri, 10 Dec 2010 16:10:50 +0100] rev 41107
moved most fundamental lemmas upwards
bulwahn [Fri, 10 Dec 2010 14:10:35 +0100] rev 41106
setting finite_type_size to 1 in mutabelle_extra
bulwahn [Fri, 10 Dec 2010 11:42:05 +0100] rev 41105
adding check_all instances for a few more finite types in smallcheck
bulwahn [Fri, 10 Dec 2010 11:42:04 +0100] rev 41104
removing unneccassary sort constraints
krauss [Fri, 10 Dec 2010 09:18:17 +0100] rev 41103
made smlnj happy
haftmann [Thu, 09 Dec 2010 17:26:08 +0100] rev 41102
merged
haftmann [Thu, 09 Dec 2010 17:25:43 +0100] rev 41101
tuned names
haftmann [Thu, 09 Dec 2010 17:25:43 +0100] rev 41100
dictionary constants must permit explicit weakening of classes;
tuned names
haftmann [Thu, 09 Dec 2010 09:58:33 +0100] rev 41099
tracing of term to be evaluated
hoelzl [Thu, 09 Dec 2010 10:22:17 +0100] rev 41098
merged
hoelzl [Wed, 08 Dec 2010 19:32:11 +0100] rev 41097
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl [Wed, 08 Dec 2010 16:15:14 +0100] rev 41096
integral over setprod
hoelzl [Wed, 08 Dec 2010 16:15:14 +0100] rev 41095
cleanup bijectivity btw. product spaces and pairs
blanchet [Thu, 09 Dec 2010 08:46:04 +0100] rev 41094
compile
blanchet [Wed, 08 Dec 2010 22:18:37 +0100] rev 41093
lower fudge factor
blanchet [Wed, 08 Dec 2010 22:17:53 +0100] rev 41092
reword error message
blanchet [Wed, 08 Dec 2010 22:17:53 +0100] rev 41091
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41090
renamings
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41089
moved function to later module
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41088
clarified terminology
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41087
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
bulwahn [Wed, 08 Dec 2010 18:07:04 +0100] rev 41086
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn [Wed, 08 Dec 2010 18:07:03 +0100] rev 41085
adding a smarter enumeration scheme for finite functions