| Tue, 22 Feb 2022 12:36:01 +0100 |
blanchet |
handle Zipperposition definitions in Isar proof construction
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 12:48:33 +0100 |
blanchet |
careful with partial applications
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 11:51:41 +0100 |
blanchet |
handle TPTP '!=' more gracefully in Isar proof reconstruction
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 22:08:51 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Mon, 19 Jul 2021 14:47:53 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 17 Dec 2020 15:31:31 +0100 |
desharna |
tweaked tptp parsing when source info is missing
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:46:03 +0200 |
blanchet |
removed obsolete unmaintained experimental prover Pirate
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 15:59:25 +0200 |
blanchet |
added support for Zipperposition on SystemOnTPTP
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 16:37:45 +0100 |
blanchet |
SPASS-Pirate is now called Pirate
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sun, 12 Oct 2014 21:52:45 +0200 |
blanchet |
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
|
file |
diff |
annotate
|
| Sun, 12 Oct 2014 21:52:44 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
avoid creating needless skolemization steps for SPASS
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
get rid of 'individual' type in DFG proofs
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
slightly nicer names
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
improved unskolemization of SPASS problems
|
file |
diff |
annotate
|
| Tue, 30 Sep 2014 16:01:46 +0200 |
blanchet |
proper types for applied variables, for typed formats (TFF0, DFG)
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 20:26:04 +0200 |
blanchet |
support hypotheses with schematics in Isar proofs
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
parse back type of SPASS proof variables
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 23:48:46 +0200 |
blanchet |
reworked unskolemization for SPASS
|
file |
diff |
annotate
|
| Sat, 09 Aug 2014 21:03:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 10:59:40 +0200 |
blanchet |
rationalize Skolem names
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 10:02:35 +0200 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 09:58:23 +0200 |
blanchet |
don't rename variables which will be renamed later anyway
|
file |
diff |
annotate
|