| 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
|