| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 12:30:54 +0100 |
blanchet |
refactor large ML file
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
tuned ML file name
|
file |
diff |
annotate
|
| Thu, 17 Oct 2013 20:49:19 +0200 |
blanchet |
generate a comment storing the goal nickname in "learn_prover"
|
file |
diff |
annotate
|
| Thu, 17 Oct 2013 01:10:08 +0200 |
blanchet |
if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
|
file |
diff |
annotate
|
| Tue, 28 May 2013 08:52:41 +0200 |
blanchet |
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
|
file |
diff |
annotate
|
| Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:50:30 +0100 |
wenzelm |
clarified Skip_Proof.cheat_tac: more standard tactic;
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned data structure
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
eliminated needless speed optimization -- and simplified code quite a bit
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML structures
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
centrally construct expensive data structures
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more code rationalization in relevance filter
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
systematize lazy names in relevance filter
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
rationalize relevance filter, slowing moving code from Iter to MaSh
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
killed one file
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 15:24:37 +0200 |
blanchet |
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 15:24:37 +0200 |
blanchet |
move file to where it belongs
|
file |
diff |
annotate
| base
|