| Thu, 22 Jun 2017 21:10:13 +0200 |
wenzelm |
consolidate proofs more simultaneously;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 21:05:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 03 Feb 2017 23:24:45 +0100 |
wenzelm |
proper background certificate from make_context, which can be a super-theory of the direct join (amending d07464875dd4);
|
file |
diff |
annotate
|
| Fri, 16 Dec 2016 19:07:16 +0100 |
wenzelm |
consolidate nested thms with persistent result, for improved performance;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2016 14:06:31 +0100 |
wenzelm |
tuned signature -- more abstract type thm_node;
|
file |
diff |
annotate
|
| Thu, 15 Dec 2016 21:16:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 15 Dec 2016 15:08:18 +0100 |
wenzelm |
back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
|
file |
diff |
annotate
|
| Wed, 14 Dec 2016 18:22:18 +0100 |
wenzelm |
more careful derivation_closed / close_derivation;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 20:31:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 16:36:03 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 17:32:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 15:43:13 +0200 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 15:21:25 +0200 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 12:17:23 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 11:56:37 +0200 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 23:48:03 +0200 |
wenzelm |
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 23:21:04 +0200 |
wenzelm |
more abstract theory certificate, which is not necessarily the full theory;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 13:37:06 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 11:53:09 +0200 |
wenzelm |
tuned signature;
|
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 20:25:12 +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
|
| Sun, 16 Aug 2015 18:19:30 +0200 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|
| Sat, 15 Aug 2015 20:27:23 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 19:49:54 +0200 |
wenzelm |
more direct access to atomic cterms;
|
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
|
| Fri, 03 Jul 2015 14:32:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 21:52:37 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 16:24:22 +0200 |
wenzelm |
explicitly checked alpha conversion -- actual renaming happens outside kernel;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|