| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
ea4853ba |
|
28-Jan-2018 |
wenzelm <none@none> |
clarified take/drop/chop prefix/suffix;
|
| #
151b7ea2 |
|
10-Apr-2017 |
wenzelm <none@none> |
tuned signature;
|
| #
48e2d74a |
|
03-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
8e8483b1 |
|
02-Jun-2014 |
blanchet <none@none> |
tuned whitespace
|
| #
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
| #
70573b75 |
|
03-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
b58b6956 |
|
31-Jan-2014 |
blanchet <none@none> |
renamed ML file
--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
|
| #
fb3c73e4 |
|
17-Oct-2013 |
blanchet <none@none> |
make sure add: doesn't add duplicates, and works for [no_atp] facts
|
| #
8219bdec |
|
17-Oct-2013 |
blanchet <none@none> |
no fact subsumption -- this only confuses later code, e.g. 'add:'
|
| #
09d5ce16 |
|
16-Oct-2013 |
blanchet <none@none> |
fast track -- avoid domain error in 0 case
|
| #
f3876dad |
|
15-Oct-2013 |
blanchet <none@none> |
drop only real duplicates, not subsumed facts -- this confuses MaSh
|
| #
a4a53b54 |
|
09-Oct-2013 |
blanchet <none@none> |
simplify fudge factor code
|
| #
d347b7b8 |
|
09-Oct-2013 |
blanchet <none@none> |
run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
|
| #
cde1e5fa |
|
09-Oct-2013 |
blanchet <none@none> |
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
|
| #
f85c74ed |
|
09-Oct-2013 |
blanchet <none@none> |
minor performance tuning
|
| #
f1ee7e18 |
|
09-Oct-2013 |
blanchet <none@none> |
use plain types instead of dedicated type pattern
|
| #
0eeee502 |
|
09-Oct-2013 |
blanchet <none@none> |
duplicate term and type patterns
|
| #
ae4d0cef |
|
11-Sep-2013 |
blanchet <none@none> |
killed dead code
|
| #
21e65e4e |
|
11-Sep-2013 |
blanchet <none@none> |
get rid of another complication in relevance filter
|
| #
4a143680 |
|
11-Sep-2013 |
blanchet <none@none> |
renamed config option
|
| #
9ca474eb |
|
11-Sep-2013 |
blanchet <none@none> |
kick out totally hopeless facts after 5 iterations to speed things up
|
| #
568812f2 |
|
11-Sep-2013 |
blanchet <none@none> |
got rid of currently unused data structure, to speed up relevance filter
|
| #
7b7e112f |
|
09-Sep-2013 |
blanchet <none@none> |
make facts like "mem_Collect_eq" more likely to be picked up by few-fact slices
|
| #
681096a3 |
|
23-Aug-2013 |
blanchet <none@none> |
thread information about when a constant became relevant through MePo -- the information is not used yet but could help fight starvation in the (ITP) world
|
| #
b336f750 |
|
21-Aug-2013 |
blanchet <none@none> |
weight MaSh constants by frequency
|
| #
801d585a |
|
15-May-2013 |
blanchet <none@none> |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
| #
8b4c3671 |
|
07-Feb-2013 |
blanchet <none@none> |
tuned indent
|
| #
7cfd79bb |
|
31-Jan-2013 |
blanchet <none@none> |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
| #
f73a7454 |
|
19-Jan-2013 |
blanchet <none@none> |
tuning
|
| #
f4986e05 |
|
20-Dec-2012 |
blanchet <none@none> |
better weight functions for MePo/MaSh etc.
|
| #
2e62a8ad |
|
05-Dec-2012 |
blanchet <none@none> |
take proximity into account for MaSh + fix a debilitating bug in feature generation
|
| #
113293b3 |
|
05-Dec-2012 |
blanchet <none@none> |
tuning
|
| #
cd384aa1 |
|
12-Nov-2012 |
blanchet <none@none> |
fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
|
| #
2e0ddacb |
|
20-Jul-2012 |
blanchet <none@none> |
tune Mesh filter
|
| #
84aa75b1 |
|
20-Jul-2012 |
blanchet <none@none> |
honor suggested MaSh weights
|
| #
7b5f817b |
|
20-Jul-2012 |
blanchet <none@none> |
renamed ML structures
|
| #
b2844097 |
|
20-Jul-2012 |
blanchet <none@none> |
renamed ML files
--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML => src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML => src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
|