| Fri, 05 Mar 2021 16:09:42 +0100 |
wenzelm |
clarified signature --- augment existing structure Time;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2020 15:18:08 +0200 |
desharna |
Tuned isar_step datatype
|
file |
diff |
annotate
|
| Wed, 21 Oct 2020 17:46:51 +0200 |
desharna |
Tuned isar_proofs constructions
|
file |
diff |
annotate
|
| Wed, 21 Oct 2020 17:31:15 +0200 |
desharna |
Tuned isar_proof datatype
|
file |
diff |
annotate
|
| Thu, 01 Feb 2018 15:12:57 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 23:29:05 +0200 |
wenzelm |
prefer infix operations;
|
file |
diff |
annotate
|
| Mon, 01 Feb 2016 19:57:58 +0100 |
blanchet |
preplaying of 'smt' and 'metis' more in sync with actual method
|
file |
diff |
annotate
|
| Sat, 14 Nov 2015 13:48:49 +0100 |
wenzelm |
more standard ML, to make SML/NJ more happy;
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 17:49:54 +0100 |
fleury |
generalized so that is also works for veriT proofs
|
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, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 12:28:42 +0200 |
blanchet |
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 23:29:50 +0200 |
blanchet |
fine-tuned Isar reconstruction, esp. boolean simplifications
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 20:44:51 +0200 |
blanchet |
careful when compressing 'obtains'
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 20:15:41 +0200 |
blanchet |
try to get rid of skolems first
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 19:32:46 +0200 |
blanchet |
no need to 'obtain' variables not in formula
|
file |
diff |
annotate
|
| Thu, 31 Jul 2014 00:45:55 +0200 |
blanchet |
cascading timeout in parallel evaluation, to rapidly find optimum
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 00:50:41 +0200 |
blanchet |
also try 'metis' with 'full_types'
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 08:19:22 +0200 |
blanchet |
don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:10:12 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 22:38:46 +0200 |
blanchet |
avoid division by 0
|
file |
diff |
annotate
|
| Thu, 22 May 2014 03:29:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 13:16:17 +0100 |
blanchet |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
file |
diff |
annotate
|
| Wed, 05 Feb 2014 11:37:32 +0100 |
blanchet |
more exception cleanup + more liberal compressions of steps that timed out
|
file |
diff |
annotate
|
| Wed, 05 Feb 2014 11:22:36 +0100 |
blanchet |
tuned code to avoid noncanonical (and risky) exception handling
|
file |
diff |
annotate
|
| Wed, 05 Feb 2014 09:25:48 +0100 |
blanchet |
got rid of indices
|
file |
diff |
annotate
|
| Wed, 05 Feb 2014 09:07:08 +0100 |
blanchet |
corrected wrong 'meth :: _' pattern maching + tuned code
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
more generous Isar proof compression -- try to remove failing steps
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
tweaked handling of 'hopeless' methods
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|