| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
added "nitrox" tool (Nitpick for first-order TPTP problems) to components
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
made one more Metis example use the new Skolemizer
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
Metis examples use the new Skolemizer to test it
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
new version of Metis 2.3 (29 Dec. 2010)
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
remove newly added wrong logic
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
more precise failure reporting in Sledgehammer/SMT
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
avoid evil "export_without_context", which breaks if there are local "fixes"
|
changeset |
files
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
more robust handling of variables in new Skolemizer
|
changeset |
files
|
| Thu, 24 Mar 2011 17:10:23 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 24 Mar 2011 17:10:13 +0100 |
haftmann |
added subsection on Scala specialities
|
changeset |
files
|
| Thu, 24 Mar 2011 16:39:37 +0100 |
krauss |
added more judgement day provers
|
changeset |
files
|
| Thu, 24 Mar 2011 15:29:31 +0100 |
bulwahn |
allowing special set comprehensions in values command; adding an example for special set comprehension in values
|
changeset |
files
|
| Thu, 24 Mar 2011 10:39:47 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:42 +0100 |
bulwahn |
adding documentation about the eval option in quickcheck
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:40 +0100 |
bulwahn |
adapting Quickcheck_Prolog to latest changes
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:39 +0100 |
bulwahn |
changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:32 +0100 |
bulwahn |
adapting mutabelle; exporting more Quickcheck functions
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:31 +0100 |
bulwahn |
making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
|
changeset |
files
|
| Wed, 23 Mar 2011 08:50:29 +0100 |
bulwahn |
changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout
|
changeset |
files
|
| Sat, 26 Mar 2011 12:01:40 +0100 |
wenzelm |
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
|
changeset |
files
|
| Sat, 26 Mar 2011 10:52:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 26 Mar 2011 10:25:17 +0100 |
wenzelm |
dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;
|
changeset |
files
|
| Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
changeset |
files
|
| Thu, 24 Mar 2011 16:47:24 +0100 |
wenzelm |
more direct loose_bvar1;
|
changeset |
files
|
| Thu, 24 Mar 2011 13:54:39 +0100 |
wenzelm |
indentation;
|
changeset |
files
|
| Thu, 24 Mar 2011 11:45:39 +0100 |
wenzelm |
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
|
changeset |
files
|
| Wed, 23 Mar 2011 21:07:05 +0100 |
wenzelm |
added editor mode line;
|
changeset |
files
|
| Wed, 23 Mar 2011 20:57:37 +0100 |
wenzelm |
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
|
changeset |
files
|
| Wed, 23 Mar 2011 20:51:36 +0100 |
wenzelm |
list Isabelle tools via perl script, which is much faster that bash plumbing, especially on Cygwin;
|
changeset |
files
|
| Wed, 23 Mar 2011 16:42:09 +0100 |
boehmes |
updated contributed components
|
changeset |
files
|