| Sat, 19 Dec 2015 20:02:51 +0100 |
blanchet |
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
|
file |
diff |
annotate
|
| Tue, 02 Jun 2015 09:16:19 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 15:29:09 +0200 |
wenzelm |
more standard Long_Name operations;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 18:27:37 +0200 |
blanchet |
tuned whitespace and parentheses
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:40:59 +0200 |
blanchet |
simplified code
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 15:22:04 +0200 |
blanchet |
move metis to new monomorphizer
|
file |
diff |
annotate
|
| Sun, 26 May 2013 12:56:37 +0200 |
blanchet |
handle lambda-lifted problems in Isar construction code
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
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
|
| Thu, 28 Mar 2013 23:44:41 +0100 |
boehmes |
new, simpler implementation of monomorphization;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 22:49:08 +0100 |
blanchet |
generate comments with original names for debugging
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
added type arguments to "ATerm" constructor -- but don't use them yet
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
started adding polymophic SPASS output
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 21 May 2012 10:39:32 +0200 |
blanchet |
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
|
file |
diff |
annotate
|
| Sun, 13 May 2012 16:31:01 +0200 |
blanchet |
get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 13:53:09 +0100 |
blanchet |
remove two options that were found to play hardly any role
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 10:06:35 +0100 |
blanchet |
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
|
file |
diff |
annotate
|
| Sat, 04 Feb 2012 12:08:18 +0100 |
blanchet |
made option available to users (mostly for experiments)
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
rename lambda translation schemes
|
file |
diff |
annotate
|
| Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
separate orthogonal components
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
| base
|