| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
fe9da3ea |
|
15-Dec-2016 |
blanchet <none@none> |
updated CASC instructions + tuning
|
| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
ec76ee03 |
|
06-Aug-2014 |
blanchet <none@none> |
make TPTP tools work on polymorphic (TFF1) problems as well
|
| #
87953653 |
|
30-Jun-2013 |
wenzelm <none@none> |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
| #
b628a60a |
|
27-Jun-2013 |
wenzelm <none@none> |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
| #
36418877 |
|
31-Oct-2012 |
blanchet <none@none> |
moved Refute to "HOL/Library" to speed up building "Main" even more
--HG--
rename : src/HOL/Refute.thy => src/HOL/Library/Refute.thy
rename : src/HOL/Tools/refute.ML => src/HOL/Library/refute.ML
|
| #
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
| #
4f850aca |
|
27-Apr-2012 |
blanchet <none@none> |
use Nitpick as an oracle for finite problems
|
| #
6ce0bd41 |
|
27-Apr-2012 |
blanchet <none@none> |
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
|
| #
1a0ddd6b |
|
27-Apr-2012 |
blanchet <none@none> |
move file to where it belongs
--HG--
rename : src/HOL/ex/sledgehammer_tactics.ML => src/HOL/TPTP/sledgehammer_tactics.ML
|
| #
2d907cd2 |
|
27-Apr-2012 |
blanchet <none@none> |
tuning
|
| #
90997541 |
|
26-Apr-2012 |
blanchet <none@none> |
more tweaking of TPTP/CASC setup
|
| #
927d3125 |
|
25-Apr-2012 |
blanchet <none@none> |
tuning
|
| #
eb9a750b |
|
25-Apr-2012 |
blanchet <none@none> |
more work on TPTP Isabelle and Sledgehammer tactics
|
| #
d99f3ac7 |
|
25-Apr-2012 |
blanchet <none@none> |
more work on CASC setup
|
| #
2c8eb630 |
|
24-Apr-2012 |
blanchet <none@none> |
get rid of old parser, hopefully for good
|
| #
8dc6a48b |
|
22-Apr-2012 |
blanchet <none@none> |
added timeout argument to TPTP tools
|
| #
16412bdd |
|
18-Apr-2012 |
blanchet <none@none> |
started integrating Nik's parser into TPTP command-line tools
|
| #
cadbf5cb |
|
23-Jan-2012 |
blanchet <none@none> |
added problem importer
|