| Fri, 19 Nov 2010 14:58:49 +0000 |
paulson |
First-order pattern matching: catch a rogue exception (differing numbers of arguments)
|
changeset |
files
|
| Fri, 19 Nov 2010 14:35:58 +0100 |
haftmann |
eval simp rules for predicate type, simplify primitive proofs
|
changeset |
files
|
| Fri, 19 Nov 2010 11:44:46 +0100 |
haftmann |
generalized type
|
changeset |
files
|
| Fri, 19 Nov 2010 10:37:06 +0100 |
haftmann |
made smlnj happy
|
changeset |
files
|
| Fri, 19 Nov 2010 10:04:08 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 18 Nov 2010 18:53:36 +0100 |
haftmann |
proper qualification needed due to shadowing on theory merge
|
changeset |
files
|
| Thu, 18 Nov 2010 17:06:02 +0100 |
haftmann |
more appropriate name for property
|
changeset |
files
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
mapper for sum type
|
changeset |
files
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
mapper for option type
|
changeset |
files
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
mapper for list type; map_pair replaces prod_fun
|
changeset |
files
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
map_pair replaces prod_fun
|
changeset |
files
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
mapper for mulitset type
|
changeset |
files
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
mapper for mapping type
|
changeset |
files
|
| Thu, 18 Nov 2010 17:01:15 +0100 |
haftmann |
mapper for fset type
|
changeset |
files
|
| Thu, 18 Nov 2010 17:01:15 +0100 |
haftmann |
mapper for dlist type
|
changeset |
files
|
| Thu, 18 Nov 2010 17:01:15 +0100 |
haftmann |
map_fun combinator in theory Fun
|
changeset |
files
|
| Thu, 18 Nov 2010 22:34:32 +0100 |
wenzelm |
some updates after 2 years of Mercurial usage;
|
changeset |
files
|
| Thu, 18 Nov 2010 18:12:03 +0100 |
blanchet |
mention Sledgehammer with SMT
|
changeset |
files
|
| Thu, 18 Nov 2010 18:09:08 +0100 |
blanchet |
enabled SMT solver in Sledgehammer by default
|
changeset |
files
|
| Thu, 18 Nov 2010 12:37:30 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 18 Nov 2010 10:59:42 +0100 |
haftmann |
keep variables bound
|
changeset |
files
|
| Thu, 18 Nov 2010 10:52:38 +0100 |
blanchet |
remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
|
changeset |
files
|
| Wed, 17 Nov 2010 23:20:26 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 17 Nov 2010 17:27:25 +0100 |
haftmann |
infer variances of user-given mapper operation; proper thm storing
|
changeset |
files
|