| 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
|
| Tue, 31 Mar 2015 20:18:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:43:03 +0100 |
wenzelm |
local fixes may depend on goal params;
|
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
|
| Wed, 04 Mar 2015 23:21:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:56:25 +0100 |
wenzelm |
removed unused;
|
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
|
| Sat, 08 Nov 2014 16:35:24 +0100 |
wenzelm |
proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 16:20:46 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 14:28:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:20:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Fri, 19 Jul 2013 17:35:12 +0200 |
wenzelm |
turned pattern unify flag into configuration option (global only);
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 13:12:54 +0200 |
wenzelm |
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
|
file |
diff |
annotate
|
| Sun, 30 Jun 2013 11:37:34 +0200 |
wenzelm |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 23:17:26 +0200 |
wenzelm |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
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
|
| Wed, 29 May 2013 16:12:05 +0200 |
wenzelm |
unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;
|
file |
diff |
annotate
|
| Fri, 24 May 2013 17:00:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 20:56:08 +0200 |
wenzelm |
updated comment to 46b90bbc370d;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 20:23:47 +0100 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 15:22:21 +0200 |
wenzelm |
proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);
|
file |
diff |
annotate
|
| Sun, 15 Jul 2012 17:53:47 +0200 |
wenzelm |
prefer canonical fold_rev;
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 22:22:01 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 25 Jan 2012 14:13:59 +0100 |
wenzelm |
removed obscure/outdated material;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 20:05:58 +0100 |
wenzelm |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
file |
diff |
annotate
|