Fri, 25 Oct 2024 15:31:58 +0200 |
blanchet |
variable instantiation in Sledgehammer and Metis
|
file |
diff |
annotate
|
Fri, 20 Sep 2024 14:28:13 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
file |
diff |
annotate
|
Wed, 07 Aug 2024 20:06:55 +0200 |
wenzelm |
more robust: only type inference with its finish/fixate phase (on contrast to dc387e3999ec), e.g. avoid accidental "improvement" of type class operations (free vs. const);
|
file |
diff |
annotate
|
Fri, 10 Dec 2021 08:53:02 +0100 |
desharna |
tuned metis to use map_index
|
file |
diff |
annotate
|
Thu, 28 Oct 2021 20:09:37 +0200 |
wenzelm |
clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;
|
file |
diff |
annotate
|
Tue, 21 Sep 2021 20:56:28 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
Sat, 11 Sep 2021 13:04:32 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
Mon, 12 Aug 2019 19:47:48 +0200 |
wenzelm |
more compact proof terms;
|
file |
diff |
annotate
|
Mon, 12 Aug 2019 18:53:02 +0200 |
wenzelm |
tuned -- avoid shadowing of ML names;
|
file |
diff |
annotate
|
Mon, 12 Aug 2019 18:00:46 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 12 Aug 2019 15:43:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 12 Aug 2019 14:39:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 12 Aug 2019 11:15:57 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 12 Aug 2019 11:04:41 +0200 |
wenzelm |
misc tuning -- slightly more readable;
|
file |
diff |
annotate
|
Thu, 08 Aug 2019 10:50:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 07 Aug 2019 17:43:48 +0200 |
wenzelm |
more compact proofterms;
|
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, 25 Feb 2018 19:43:38 +0100 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
Mon, 08 Jan 2018 16:45:30 +0100 |
wenzelm |
prefer qualified names;
|
file |
diff |
annotate
|
Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Fri, 05 Aug 2016 20:26:13 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
Mon, 27 Jul 2015 11:30:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 27 Jul 2015 00:17:18 +0200 |
wenzelm |
added infer_instantiate_vars, which allows inconsistent types for variables, as required for Metis proof reconstruction;
|
file |
diff |
annotate
|
Sat, 25 Jul 2015 23:41:53 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|