| Fri, 03 Dec 2010 18:29:14 +0100 |
blanchet |
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
|
changeset |
files
|
| Fri, 03 Dec 2010 18:27:21 +0100 |
blanchet |
export more information about available SMT solvers
|
changeset |
files
|
| Fri, 03 Dec 2010 17:59:13 +0100 |
wenzelm |
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
|
changeset |
files
|
| Thu, 02 Dec 2010 21:48:36 +0100 |
traytel |
use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
|
changeset |
files
|
| Fri, 03 Dec 2010 17:31:27 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Fri, 03 Dec 2010 17:29:27 +0100 |
wenzelm |
removed confusing comments (cf. 500171e7aa59);
|
changeset |
files
|
| Fri, 03 Dec 2010 17:18:41 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 03 Dec 2010 14:00:55 +0100 |
haftmann |
removed outdated lint script
|
changeset |
files
|
| Fri, 03 Dec 2010 10:43:09 +0100 |
blanchet |
merged
|
changeset |
files
|
| Fri, 03 Dec 2010 10:28:39 +0100 |
blanchet |
compile
|
changeset |
files
|
| Fri, 03 Dec 2010 09:55:45 +0100 |
blanchet |
run synchronous Auto Tools in parallel
|
changeset |
files
|
| Fri, 03 Dec 2010 10:17:55 +0100 |
krauss |
really fixed comment (cf. 7abeb749ae99)
|
changeset |
files
|
| Fri, 03 Dec 2010 10:03:13 +0100 |
huffman |
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
|
changeset |
files
|
| Fri, 03 Dec 2010 10:03:10 +0100 |
krauss |
eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended
|
changeset |
files
|
| Fri, 03 Dec 2010 09:58:32 +0100 |
bulwahn |
NEWS
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
only instantiate type variable if there exists some in quickcheck
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
fixing comment in library
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adapting predicate_compile_quickcheck
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adding a nice definition of Id_on for quickcheck and nitpick
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adding code equation for finiteness of finite types
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
improving sledgehammer_tactic and adding relevance filtering to the tactic
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adapting mutabelle
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adapting SML_Quickcheck to recent changes
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
explaining quickcheck testers in the documentation
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adapting quickcheck examples
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
improving presentation of quickcheck reports
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
declaring quickcheck testers as default after their setup
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
activating construction of exhaustive testing combinators
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
renamed generator into exhaustive
|
changeset |
files
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
checking if parameter is name of a tester which allows e.g. quickcheck[random]
|
changeset |
files
|