| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Tue, 06 Aug 2019 16:29:28 +0200 |
wenzelm |
more robust and convenient treatment of implicit context;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2019 11:23:09 +0200 |
wenzelm |
clarified modules: inference kernel maintains sort algebra within the logic;
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 21:43:41 +0200 |
wenzelm |
meson: more cterm operations;
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 16:42:19 +0200 |
wenzelm |
tuned signature -- more ctyp operations;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2018 16:40:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 22:39:39 +0200 |
wenzelm |
clarified standardization of variables, with proper treatment of local variables;
|
file |
diff |
annotate
|
| Mon, 06 Aug 2018 11:06:43 +0200 |
wenzelm |
export shyps as regular typargs;
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 14:19:52 +0200 |
wenzelm |
disallow hyps in export;
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 15:42:52 +0200 |
wenzelm |
unfold is subject to unfold_abs_def (still inactive);
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:03:24 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Tue, 15 Dec 2015 16:57:10 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 21:55:11 +0200 |
wenzelm |
produce certified vars without access to theory_of_thm, and without context;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 21:47:03 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 21:10:41 +0200 |
wenzelm |
clarified Variable.gen_all;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 20:59:39 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 19:49:54 +0200 |
wenzelm |
more direct access to atomic cterms;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 23:40:39 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 15:13:05 +0200 |
wenzelm |
more explicit checks -- improved errors;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 14:56:06 +0200 |
wenzelm |
eliminated cterm_instantiate;
|
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
|
| Sun, 26 Jul 2015 20:54:02 +0200 |
wenzelm |
ignore non-existant variables, like other instantiate rules;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 12:24:16 +0200 |
wenzelm |
added infer_instantiate';
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 11:08:57 +0200 |
wenzelm |
more uniform exceptions, like cterm_instantiate;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2015 23:15:37 +0200 |
wenzelm |
more accurate maxidx;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2015 21:54:09 +0200 |
wenzelm |
clarified error;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2015 21:37:09 +0200 |
wenzelm |
added infer_instantiate, which is meant to supersede cterm_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
|
| Wed, 03 Jun 2015 19:25:05 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sun, 31 May 2015 00:20:35 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Sun, 31 May 2015 00:11:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 23:58:06 +0200 |
wenzelm |
standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 22:04:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 21:52:37 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 21:28:01 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 20:21:53 +0200 |
wenzelm |
tuned -- more direct Thm.renamed_prop;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 16:44:38 +0200 |
wenzelm |
suppress formal sort-constraints, in accordance to norm_hhf_eqs;
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 11:29:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 22 Mar 2015 12:38:41 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2015 11:09:08 +0100 |
wenzelm |
tuned -- prepare instantiation more uniformly;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 21:32:31 +0100 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 13:28:04 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 23:21:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 15:43:45 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 17:06:22 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 11:33:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 May 2013 18:52:35 +0200 |
wenzelm |
more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);
|
file |
diff |
annotate
|
| Wed, 29 May 2013 18:25:11 +0200 |
wenzelm |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
file |
diff |
annotate
|