src/HOL/Tools/Metis/metis_reconstruct.ML
Fri, 25 Oct 2024 15:31:58 +0200 blanchet variable instantiation in Sledgehammer and Metis
Fri, 20 Sep 2024 14:28:13 +0200 wenzelm clarified signature: more explicit operations;
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);
Fri, 10 Dec 2021 08:53:02 +0100 desharna tuned metis to use map_index
Thu, 28 Oct 2021 20:09:37 +0200 wenzelm clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;
Tue, 21 Sep 2021 20:56:28 +0200 wenzelm clarified antiquotations;
Sat, 11 Sep 2021 13:04:32 +0200 wenzelm more antiquotations;
Fri, 10 Sep 2021 14:59:19 +0200 wenzelm clarified signature: more scalable operations;
Mon, 12 Aug 2019 19:47:48 +0200 wenzelm more compact proof terms;
Mon, 12 Aug 2019 18:53:02 +0200 wenzelm tuned -- avoid shadowing of ML names;
Mon, 12 Aug 2019 18:00:46 +0200 wenzelm tuned;
Mon, 12 Aug 2019 15:43:05 +0200 wenzelm tuned;
Mon, 12 Aug 2019 14:39:55 +0200 wenzelm tuned;
Mon, 12 Aug 2019 11:15:57 +0200 wenzelm tuned;
Mon, 12 Aug 2019 11:04:41 +0200 wenzelm misc tuning -- slightly more readable;
Thu, 08 Aug 2019 10:50:23 +0200 wenzelm tuned;
Wed, 07 Aug 2019 17:43:48 +0200 wenzelm more compact proofterms;
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 25 Feb 2018 19:43:38 +0100 wenzelm prefer symbols;
Mon, 08 Jan 2018 16:45:30 +0100 wenzelm prefer qualified names;
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Fri, 05 Aug 2016 20:26:13 +0200 wenzelm tuned;
Fri, 27 May 2016 20:23:55 +0200 wenzelm tuned proofs, to allow unfold_abs_def;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Sun, 16 Aug 2015 19:25:08 +0200 wenzelm added Thm.chyps_of;
Mon, 27 Jul 2015 11:30:10 +0200 wenzelm tuned signature;
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;
Sat, 25 Jul 2015 23:41:53 +0200 wenzelm updated to infer_instantiate;
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);
less more (0) -100 -50 -30 tip