src/Pure/drule.ML
Sun, 31 Dec 2023 22:39:40 +0100 wenzelm minor performance tuning: proper Same.operation;
Wed, 18 Oct 2023 15:13:52 +0200 wenzelm clarified signature: more concise variations on implicit theory setup;
Tue, 06 Jun 2023 11:33:38 +0200 wenzelm tuned;
Mon, 15 May 2023 10:59:49 +0200 wenzelm tuned: more accurate check (is_norm_hhf protect);
Tue, 18 Apr 2023 22:24:48 +0200 wenzelm tuned;
Fri, 10 Sep 2021 14:59:19 +0200 wenzelm clarified signature: more scalable operations;
Thu, 09 Sep 2021 17:20:41 +0200 wenzelm clarified signature;
Thu, 09 Sep 2021 12:33:14 +0200 wenzelm clarified signature;
Mon, 06 Sep 2021 14:05:22 +0200 wenzelm clarified modules;
Mon, 06 Sep 2021 12:23:06 +0200 wenzelm clarified modules;
Mon, 06 Sep 2021 12:11:17 +0200 wenzelm clarified signature;
Mon, 06 Sep 2021 11:55:54 +0200 wenzelm more scalable operations;
Mon, 06 Sep 2021 11:32:18 +0200 wenzelm more efficient operations: traverse hyps only when required;
Sun, 05 Sep 2021 21:09:31 +0200 wenzelm more scalable operations;
Sun, 05 Sep 2021 19:47:06 +0200 wenzelm unused;
Sat, 04 Sep 2021 22:17:15 +0200 wenzelm tuned signature;
Sat, 04 Sep 2021 22:05:35 +0200 wenzelm clarified signature;
Sat, 04 Sep 2021 21:25:08 +0200 wenzelm clarified signature;
Sat, 04 Sep 2021 18:21:58 +0200 wenzelm more scalable operations;
Fri, 03 Sep 2021 18:57:33 +0200 wenzelm more scalable data structure (but: rarely used many arguments);
Thu, 26 Aug 2021 14:45:19 +0200 wenzelm more scalable data structure (but: rarely used with > 5 arguments);
Fri, 09 Aug 2019 17:14:49 +0200 wenzelm formal position for PThm nodes;
Tue, 06 Aug 2019 16:29:28 +0200 wenzelm more robust and convenient treatment of implicit context;
Fri, 02 Aug 2019 11:23:09 +0200 wenzelm clarified modules: inference kernel maintains sort algebra within the logic;
Sat, 13 Apr 2019 21:43:41 +0200 wenzelm meson: more cterm operations;
Sat, 13 Apr 2019 16:42:19 +0200 wenzelm tuned signature -- more ctyp operations;
Mon, 01 Oct 2018 16:40:45 +0200 wenzelm tuned;
Thu, 20 Sep 2018 22:39:39 +0200 wenzelm clarified standardization of variables, with proper treatment of local variables;
Mon, 06 Aug 2018 11:06:43 +0200 wenzelm export shyps as regular typargs;
Fri, 29 Jun 2018 14:19:52 +0200 wenzelm disallow hyps in export;
Sun, 25 Feb 2018 15:44:46 +0100 wenzelm eliminated ASCII syntax from Pure bootstrap;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Thu, 28 Apr 2016 15:42:52 +0200 wenzelm unfold is subject to unfold_abs_def (still inactive);
Tue, 05 Apr 2016 20:03:24 +0200 wenzelm clarified modules -- simplified bootstrap;
Tue, 15 Dec 2015 16:57:10 +0100 wenzelm tuned signature -- clarified modules;
Sun, 16 Aug 2015 21:55:11 +0200 wenzelm produce certified vars without access to theory_of_thm, and without context;
Sun, 16 Aug 2015 19:25:08 +0200 wenzelm added Thm.chyps_of;
Tue, 28 Jul 2015 21:47:03 +0200 wenzelm more explicit context;
Tue, 28 Jul 2015 21:10:41 +0200 wenzelm clarified Variable.gen_all;
Tue, 28 Jul 2015 20:59:39 +0200 wenzelm more explicit context;
Tue, 28 Jul 2015 19:49:54 +0200 wenzelm more direct access to atomic cterms;
Mon, 27 Jul 2015 23:40:39 +0200 wenzelm tuned signature;
Mon, 27 Jul 2015 17:44:55 +0200 wenzelm tuned signature;
Mon, 27 Jul 2015 15:13:05 +0200 wenzelm more explicit checks -- improved errors;
Mon, 27 Jul 2015 14:56:06 +0200 wenzelm eliminated cterm_instantiate;
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;
Sun, 26 Jul 2015 20:54:02 +0200 wenzelm ignore non-existant variables, like other instantiate rules;
Sun, 26 Jul 2015 12:24:16 +0200 wenzelm added infer_instantiate';
Sun, 26 Jul 2015 11:08:57 +0200 wenzelm more uniform exceptions, like cterm_instantiate;
Sat, 25 Jul 2015 23:15:37 +0200 wenzelm more accurate maxidx;
Sat, 25 Jul 2015 21:54:09 +0200 wenzelm clarified error;
Sat, 25 Jul 2015 21:37:09 +0200 wenzelm added infer_instantiate, which is meant to supersede cterm_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);
Wed, 03 Jun 2015 19:25:05 +0200 wenzelm clarified context;
Sun, 31 May 2015 00:20:35 +0200 wenzelm obsolete;
Sun, 31 May 2015 00:11:12 +0200 wenzelm tuned;
Sat, 30 May 2015 23:58:06 +0200 wenzelm standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
Sat, 30 May 2015 22:04:15 +0200 wenzelm tuned;
Sat, 30 May 2015 21:52:37 +0200 wenzelm more explicit context;
less more (0) -300 -100 -60 tip