Tue, 27 Oct 2009 09:03:56 +0100 |
bulwahn |
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
|
changeset |
files
|
Tue, 27 Oct 2009 09:03:56 +0100 |
bulwahn |
adding test case for inlining of predicate compiler
|
changeset |
files
|
Tue, 27 Oct 2009 09:03:56 +0100 |
bulwahn |
hiding randompred definitions
|
changeset |
files
|
Tue, 27 Oct 2009 09:03:56 +0100 |
bulwahn |
changes to example file
|
changeset |
files
|
Tue, 27 Oct 2009 09:03:56 +0100 |
bulwahn |
print retrieved specification when printing intermediate results
|
changeset |
files
|
Tue, 27 Oct 2009 09:03:56 +0100 |
bulwahn |
added option show_modes to predicate compiler
|
changeset |
files
|
Tue, 27 Oct 2009 09:02:22 +0100 |
bulwahn |
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
|
changeset |
files
|
Tue, 27 Oct 2009 18:09:11 +0100 |
boehmes |
removed unused file smt_builtin.ML,
|
changeset |
files
|
Tue, 27 Oct 2009 18:01:50 +0100 |
boehmes |
included description for sledgehammer options in Mirabelle script
|
changeset |
files
|
Tue, 27 Oct 2009 18:00:50 +0100 |
boehmes |
measure runtime of ATPs only if requested
|
changeset |
files
|
Tue, 27 Oct 2009 22:57:23 +0100 |
wenzelm |
eliminated some old folds;
|
changeset |
files
|
Tue, 27 Oct 2009 22:56:14 +0100 |
wenzelm |
eliminated some old folds;
|
changeset |
files
|
Tue, 27 Oct 2009 22:55:27 +0100 |
wenzelm |
Datatype.read_typ: standard argument order;
|
changeset |
files
|
Tue, 27 Oct 2009 17:34:00 +0100 |
wenzelm |
normalized basic type abbreviations;
|
changeset |
files
|
Tue, 27 Oct 2009 17:19:31 +0100 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|