| Wed, 23 Mar 2011 10:06:27 +0100 |
blanchet |
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
|
changeset |
files
|
| Wed, 23 Mar 2011 10:21:29 +0100 |
boehmes |
really be quiet
|
changeset |
files
|
| Wed, 23 Mar 2011 09:15:49 +0100 |
krauss |
replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH
|
changeset |
files
|
| Tue, 22 Mar 2011 21:22:50 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 22 Mar 2011 20:06:10 +0100 |
hoelzl |
standardized headers
|
changeset |
files
|
| Tue, 22 Mar 2011 18:53:05 +0100 |
hoelzl |
generalized Caratheodory from algebra to ring_of_sets
|
changeset |
files
|
| Tue, 22 Mar 2011 16:44:57 +0100 |
hoelzl |
add ring_of_sets and subset_class as basis for algebra
|
changeset |
files
|
| Tue, 22 Mar 2011 19:04:32 +0100 |
blanchet |
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
|
changeset |
files
|
| Tue, 22 Mar 2011 18:38:29 +0100 |
blanchet |
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
|
changeset |
files
|
| Tue, 22 Mar 2011 18:27:47 +0100 |
blanchet |
remove lie from documentation
|
changeset |
files
|
| Tue, 22 Mar 2011 17:20:54 +0100 |
blanchet |
let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
|
changeset |
files
|
| Tue, 22 Mar 2011 17:20:53 +0100 |
blanchet |
make Minimizer honor "verbose" and "debug" options better
|
changeset |
files
|
| Tue, 22 Mar 2011 12:49:07 +0100 |
nipkow |
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
|
changeset |
files
|
| Mon, 21 Mar 2011 21:10:29 +0100 |
krauss |
moved some configurations to AFP, and fixed others
|
changeset |
files
|