| Tue, 27 Jul 2021 13:39:18 +0200 |
desharna |
tuned Mirabelle's theory selection
|
file |
diff |
annotate
|
| Thu, 17 Jun 2021 10:30:07 +0200 |
desharna |
changed Mirabelle's filter to use short theory names
|
file |
diff |
annotate
|
| Sat, 12 Jun 2021 15:37:25 +0200 |
desharna |
added support for unbounded max calls to Mirabelle
|
file |
diff |
annotate
|
| Sat, 12 Jun 2021 12:39:33 +0200 |
desharna |
added warnings when defining unamed or redefining Mirabelle action
|
file |
diff |
annotate
|
| Sat, 12 Jun 2021 12:16:19 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Fri, 11 Jun 2021 09:33:43 +0200 |
desharna |
tuned Mirabelle
|
file |
diff |
annotate
|
| Thu, 10 Jun 2021 11:54:14 +0200 |
desharna |
merged
|
file |
diff |
annotate
|
| Thu, 10 Jun 2021 11:21:57 +0200 |
desharna |
refactored Mirabelle to produce output in real time
|
file |
diff |
annotate
|
| Mon, 07 Jun 2021 09:27:01 +0200 |
wenzelm |
more robust within session "HOL";
|
file |
diff |
annotate
|
| Sun, 06 Jun 2021 21:17:23 +0200 |
wenzelm |
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
|
file |
diff |
annotate
|
| Sun, 06 Jun 2021 20:29:52 +0200 |
wenzelm |
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
|
file |
diff |
annotate
|
| Sun, 06 Jun 2021 16:34:57 +0200 |
wenzelm |
refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories;
|
file |
diff |
annotate
|
| Fri, 04 Jun 2021 23:55:35 +0200 |
wenzelm |
tuned --- reduced source complexity;
|
file |
diff |
annotate
|
| Fri, 04 Jun 2021 23:03:12 +0200 |
desharna |
moved stride option from sledgehammer action to main mirabelle
|
file |
diff |
annotate
|
| Sat, 15 May 2021 22:06:05 +0200 |
wenzelm |
reactive "sledgehammer";
|
file |
diff |
annotate
|
| Sat, 15 May 2021 13:25:52 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 14 May 2021 21:32:11 +0200 |
wenzelm |
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
|
file |
diff |
annotate
| base
|