| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed '_new' sufffix in SMT2 solver names (in some cases)
|
file |
diff |
annotate
|
| Fri, 04 Oct 2013 14:35:00 +0200 |
blanchet |
prevent explosion in monomorphizer (e.g. when the facts typerep_int_def typerep_num_def typerep_option_def typerep_node_def are selected)
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 19:15:50 +0200 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 16:21:03 +0200 |
blanchet |
when "max_thm_instances" is hit, choose more carefully which instances should be kept
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 18:14:54 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 18:12:41 +0200 |
blanchet |
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 15:22:04 +0200 |
blanchet |
limit the number of instances of a single theorem
|
file |
diff |
annotate
|
| Thu, 28 Mar 2013 23:44:41 +0100 |
boehmes |
new, simpler implementation of monomorphization;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 11:28:10 +0200 |
boehmes |
filter out all schematic theorems if the problem contains no ground constants
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 11:59:45 +0200 |
boehmes |
only collect substituions neither seen before nor derived in the same refinement step
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 21:37:40 +0200 |
boehmes |
clarified (and slightly modified) the semantics of max_new_instances
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 11:05:09 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 10:46:09 +0200 |
blanchet |
removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 10:24:16 +0200 |
boehmes |
clarified meaning of monomorphization configuration option by renaming it
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 07:44:54 +0200 |
blanchet |
added (currently unused) verbose configuration option
|
file |
diff |
annotate
|
| Tue, 31 May 2011 19:27:19 +0200 |
boehmes |
proper nesting of loops in new monomorphizer;
|
file |
diff |
annotate
|
| Tue, 31 May 2011 19:21:20 +0200 |
boehmes |
use new monomorphizer for SMT;
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
fixed comment
|
file |
diff |
annotate
|
| Fri, 27 May 2011 16:45:24 +0200 |
boehmes |
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
|
file |
diff |
annotate
|