| Mon, 08 Mar 2021 09:11:09 +0100 |
\----- start update Isabelle2020 --> Isabelle2021
|
file | diff | annotate |
| Wed, 23 Sep 2020 15:18:07 +0200 |
\----- start update Isabelle2019 --> Isabelle2020
|
file | diff | annotate |
| Tue, 03 Sep 2019 16:10:31 +0200 |
\----- start update Isabelle2018 --> Isabelle2019
|
file | diff | annotate |
| Wed, 22 Aug 2018 14:44:15 +0200 |
\----- start update Isabelle2017 --> Isabelle2018
|
file | diff | annotate |
| Fri, 19 Jan 2018 12:49:17 +0100 |
\----- start update Isabelle2015 --> Isabelle2017
|
file | diff | annotate |
| Sat, 05 Dec 2015 16:09:41 +0100 |
switched from Isabelle2014 to Isabelle2015, intermediate state
|
file | diff | annotate |
| Sat, 11 Apr 2015 11:28:31 +0200 |
merged
|
file | diff | annotate |
| Thu, 24 Jul 2014 18:46:38 +0200 |
refined filter for ATP steps to avoid 'have True' steps in E proofs
|
file | diff | annotate |
| Thu, 24 Jul 2014 18:46:38 +0200 |
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
|
file | diff | annotate |
| Tue, 24 Jun 2014 08:19:22 +0200 |
supports gradual skolemization (cf. Z3) by threading context through correctly
|
file | diff | annotate |
| Tue, 24 Jun 2014 08:19:22 +0200 |
given two one-liners, only show the best of the two
|
file | diff | annotate |
| Tue, 24 Jun 2014 08:19:22 +0200 |
don't generate Isar proof skeleton for what amounts to a one-line proof
|
file | diff | annotate |
| Thu, 12 Jun 2014 17:10:12 +0200 |
renamed Sledgehammer options
|
file | diff | annotate |
| Mon, 02 Jun 2014 15:10:18 +0200 |
basic setup for zipperposition prover
|
file | diff | annotate |
| Thu, 22 May 2014 05:23:50 +0200 |
properly reconstruct helpers in Z3 proofs
|
file | diff | annotate |
| Thu, 22 May 2014 03:29:36 +0200 |
tuning
|
file | diff | annotate |
| Fri, 16 May 2014 19:14:00 +0200 |
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
|
file | diff | annotate |
| Fri, 16 May 2014 19:13:50 +0200 |
use 'simp add:' syntax in Sledgehammer rather than 'using'
|
file | diff | annotate |
| Sun, 04 May 2014 19:01:36 +0200 |
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
|
file | diff | annotate |
| Fri, 14 Mar 2014 11:44:11 +0100 |
consolidate consecutive steps that prove the same formula
|
file | diff | annotate |
| Fri, 14 Mar 2014 11:15:46 +0100 |
undo rewrite rules (e.g. for 'fun_app') in Isar
|
file | diff | annotate |
| Fri, 14 Mar 2014 11:05:45 +0100 |
debugging stuff
|
file | diff | annotate |
| Fri, 14 Mar 2014 11:05:44 +0100 |
more simplification of trivial steps
|
file | diff | annotate |
| Fri, 14 Mar 2014 11:05:37 +0100 |
tuning
|
file | diff | annotate |
| Thu, 13 Mar 2014 13:18:14 +0100 |
tuning
|
file | diff | annotate |
| Thu, 13 Mar 2014 13:18:14 +0100 |
simplified preplaying information
|
file | diff | annotate |
| Thu, 13 Mar 2014 13:18:13 +0100 |
integrate SMT2 with Sledgehammer
|
file | diff | annotate |
| Thu, 06 Mar 2014 10:12:47 +0100 |
tuned signature;
|
file | diff | annotate |
| Thu, 13 Feb 2014 13:16:17 +0100 |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
file | diff | annotate |
| Tue, 04 Feb 2014 23:11:18 +0100 |
more generous Isar proof compression -- try to remove failing steps
|
file | diff | annotate |
| Tue, 04 Feb 2014 23:11:18 +0100 |
do a second phase of proof compression after minimization
|
file | diff | annotate |
| Tue, 04 Feb 2014 23:11:18 +0100 |
tuned code
|
file | diff | annotate |
| Tue, 04 Feb 2014 23:11:18 +0100 |
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
|
file | diff | annotate |
| Mon, 03 Feb 2014 23:59:36 +0100 |
rationalized lists of methods
|
file | diff | annotate |
| Mon, 03 Feb 2014 23:49:01 +0100 |
extended method list
|
file | diff | annotate |
| Mon, 03 Feb 2014 19:32:02 +0100 |
generate comments in Isar proofs
|
file | diff | annotate |
| Mon, 03 Feb 2014 19:32:02 +0100 |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file | diff | annotate |
| Mon, 03 Feb 2014 19:32:02 +0100 |
tuned behavior of 'smt' option
|
file | diff | annotate |
| Mon, 03 Feb 2014 19:32:02 +0100 |
proper fresh name generation
|
file | diff | annotate |
| Mon, 03 Feb 2014 17:13:31 +0100 |
added 'smt' option to control generation of 'by smt' proofs
|
file | diff | annotate |
| Mon, 03 Feb 2014 16:53:58 +0100 |
renamed ML file
|
file | diff | annotate |
| Mon, 03 Feb 2014 15:33:18 +0100 |
tuning
|
file | diff | annotate |
| Mon, 03 Feb 2014 15:19:07 +0100 |
merged 'reconstructors' and 'proof methods'
|
file | diff | annotate |
| Mon, 03 Feb 2014 13:37:23 +0100 |
tuning
|
file | diff | annotate |
| Mon, 03 Feb 2014 11:58:38 +0100 |
tuned data structure
|
file | diff | annotate |
| Mon, 03 Feb 2014 11:37:48 +0100 |
tuned data structure
|
file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 |
less aggressive evaluation
|
file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 |
added a new version of 'metis' to the mix
|
file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 |
implemented new 'try0_isar' semantics
|
file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 |
got rid of 'try0' step that is now redundant
|
file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 |
centralize more preplaying
|
file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 |
centralize preplaying
|
file | diff | annotate |
| Mon, 03 Feb 2014 10:14:18 +0100 |
tuned
|
file | diff | annotate |
| Sun, 02 Feb 2014 20:53:51 +0100 |
more data structure rationalization
|
file | diff | annotate |
| Sun, 02 Feb 2014 20:53:51 +0100 |
more data structure rationalization
|
file | diff | annotate |
| Sun, 02 Feb 2014 20:53:51 +0100 |
rationalized threading of 'metis' arguments
|
file | diff | annotate |
| Sun, 02 Feb 2014 20:53:51 +0100 |
refactored data structure (step 3)
|
file | diff | annotate |
| Sun, 02 Feb 2014 20:53:51 +0100 |
unform treatment of preplay_timeout = 0 and > 0
|
file | diff | annotate |
| Sun, 02 Feb 2014 20:53:51 +0100 |
use Skolem proof methods appropriately
|
file | diff | annotate |
| Sun, 02 Feb 2014 20:53:51 +0100 |
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
|
file | diff | annotate |