Wed, 08 Dec 2010 19:32:11 +0100 use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl [Wed, 08 Dec 2010 19:32:11 +0100] rev 41097
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
Wed, 08 Dec 2010 16:15:14 +0100 integral over setprod
hoelzl [Wed, 08 Dec 2010 16:15:14 +0100] rev 41096
integral over setprod
Wed, 08 Dec 2010 16:15:14 +0100 cleanup bijectivity btw. product spaces and pairs
hoelzl [Wed, 08 Dec 2010 16:15:14 +0100] rev 41095
cleanup bijectivity btw. product spaces and pairs
Thu, 09 Dec 2010 08:46:04 +0100 compile
blanchet [Thu, 09 Dec 2010 08:46:04 +0100] rev 41094
compile
Wed, 08 Dec 2010 22:18:37 +0100 lower fudge factor
blanchet [Wed, 08 Dec 2010 22:18:37 +0100] rev 41093
lower fudge factor
Wed, 08 Dec 2010 22:17:53 +0100 reword error message
blanchet [Wed, 08 Dec 2010 22:17:53 +0100] rev 41092
reword error message
Wed, 08 Dec 2010 22:17:53 +0100 implicitly call the minimizer for SMT solvers that don't return an unsat core
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
Wed, 08 Dec 2010 22:17:52 +0100 renamings
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41090
renamings
Wed, 08 Dec 2010 22:17:52 +0100 moved function to later module
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41089
moved function to later module
Wed, 08 Dec 2010 22:17:52 +0100 clarified terminology
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41088
clarified terminology
Wed, 08 Dec 2010 22:17:52 +0100 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41087
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
Wed, 08 Dec 2010 18:07:04 +0100 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:04 +0100] rev 41086
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
Wed, 08 Dec 2010 18:07:03 +0100 adding a smarter enumeration scheme for finite functions
bulwahn [Wed, 08 Dec 2010 18:07:03 +0100] rev 41085
adding a smarter enumeration scheme for finite functions
Wed, 08 Dec 2010 16:47:57 +0100 merged
haftmann [Wed, 08 Dec 2010 16:47:57 +0100] rev 41084
merged
Wed, 08 Dec 2010 16:47:45 +0100 work around problems with eta-expansion of equations
haftmann [Wed, 08 Dec 2010 16:47:45 +0100] rev 41083
work around problems with eta-expansion of equations
Wed, 08 Dec 2010 15:05:46 +0100 bot comes before top, inf before sup etc.
haftmann [Wed, 08 Dec 2010 15:05:46 +0100] rev 41082
bot comes before top, inf before sup etc.
Wed, 08 Dec 2010 14:52:23 +0100 tuned
haftmann [Wed, 08 Dec 2010 14:52:23 +0100] rev 41081
tuned
Wed, 08 Dec 2010 14:52:23 +0100 nice syntax for lattice INFI, SUPR;
haftmann [Wed, 08 Dec 2010 14:52:23 +0100] rev 41080
nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules
Wed, 08 Dec 2010 14:52:23 +0100 NEWS
haftmann [Wed, 08 Dec 2010 14:52:23 +0100] rev 41079
NEWS
Wed, 08 Dec 2010 14:25:08 +0100 adding more efficient implementations for quantifiers in Enum
bulwahn [Wed, 08 Dec 2010 14:25:08 +0100] rev 41078
adding more efficient implementations for quantifiers in Enum
Wed, 08 Dec 2010 14:25:07 +0100 improving the mutabelle script
bulwahn [Wed, 08 Dec 2010 14:25:07 +0100] rev 41077
improving the mutabelle script
Wed, 08 Dec 2010 13:34:51 +0100 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`;
haftmann [Wed, 08 Dec 2010 13:34:51 +0100] rev 41076
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`; tuned
Wed, 08 Dec 2010 13:34:50 +0100 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann [Wed, 08 Dec 2010 13:34:50 +0100] rev 41075
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
Wed, 08 Dec 2010 13:34:50 +0100 hide popular names R and B
haftmann [Wed, 08 Dec 2010 13:34:50 +0100] rev 41074
hide popular names R and B
Wed, 08 Dec 2010 08:33:04 +0100 built-in numbers are also built-in terms
boehmes [Wed, 08 Dec 2010 08:33:04 +0100] rev 41073
built-in numbers are also built-in terms
Wed, 08 Dec 2010 08:33:02 +0100 be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes [Wed, 08 Dec 2010 08:33:02 +0100] rev 41072
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
Tue, 07 Dec 2010 21:58:36 +0100 merged
haftmann [Tue, 07 Dec 2010 21:58:36 +0100] rev 41071
merged
Tue, 07 Dec 2010 16:33:54 +0100 more concise case names; proved extensionality
haftmann [Tue, 07 Dec 2010 16:33:54 +0100] rev 41070
more concise case names; proved extensionality
Tue, 07 Dec 2010 16:33:54 +0100 name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann [Tue, 07 Dec 2010 16:33:54 +0100] rev 41069
name filter operation just filter (c.f. List.filter and list comprehension syntax)
Tue, 07 Dec 2010 21:32:47 +0100 tuned whitespace
haftmann [Tue, 07 Dec 2010 21:32:47 +0100] rev 41068
tuned whitespace
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip