src/Pure/thm.ML
Thu, 15 Dec 2016 15:08:18 +0100 wenzelm back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
Wed, 14 Dec 2016 18:22:18 +0100 wenzelm more careful derivation_closed / close_derivation;
Mon, 12 Sep 2016 20:31:28 +0200 wenzelm tuned;
Fri, 05 Aug 2016 16:36:03 +0200 wenzelm tuned whitespace;
Sun, 30 Aug 2015 17:32:50 +0200 wenzelm tuned;
Sun, 30 Aug 2015 15:43:13 +0200 wenzelm clarified exceptions;
Sun, 30 Aug 2015 15:21:25 +0200 wenzelm clarified exceptions;
Sun, 30 Aug 2015 12:17:23 +0200 wenzelm trim context for persistent storage;
Sun, 30 Aug 2015 11:56:37 +0200 wenzelm clarified exceptions;
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);
Fri, 28 Aug 2015 23:21:04 +0200 wenzelm more abstract theory certificate, which is not necessarily the full theory;
Fri, 28 Aug 2015 13:37:06 +0200 wenzelm tuned signature;
Fri, 28 Aug 2015 11:53:09 +0200 wenzelm tuned signature;
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 20:25:12 +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;
Sun, 16 Aug 2015 18:19:30 +0200 wenzelm prefer theory_id operations;
Sat, 15 Aug 2015 20:27:23 +0200 wenzelm obsolete;
Tue, 28 Jul 2015 19:49:54 +0200 wenzelm more direct access to atomic cterms;
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);
Fri, 03 Jul 2015 14:32:55 +0200 wenzelm tuned signature;
Sat, 30 May 2015 21:52:37 +0200 wenzelm more explicit context;
Wed, 08 Apr 2015 16:24:22 +0200 wenzelm explicitly checked alpha conversion -- actual renaming happens outside kernel;
Fri, 03 Apr 2015 19:56:51 +0200 wenzelm more uniform "verbose" option to print name space;
Tue, 31 Mar 2015 20:18:10 +0200 wenzelm tuned signature;
Mon, 23 Mar 2015 19:43:03 +0100 wenzelm local fixes may depend on goal params;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 23:21:09 +0100 wenzelm tuned signature;
Wed, 04 Mar 2015 22:56:25 +0100 wenzelm removed unused;
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Sat, 08 Nov 2014 21:31:51 +0100 wenzelm optional proof context for unify operations, for the sake of proper local options;
Sat, 08 Nov 2014 16:35:24 +0100 wenzelm proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);
Thu, 30 Oct 2014 16:20:46 +0100 wenzelm eliminated aliases;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Tue, 11 Mar 2014 14:28:39 +0100 wenzelm tuned signature;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Tue, 30 Jul 2013 15:20:38 +0200 wenzelm tuned;
Tue, 30 Jul 2013 15:09:25 +0200 wenzelm type theory is purely value-oriented;
Fri, 19 Jul 2013 17:35:12 +0200 wenzelm turned pattern unify flag into configuration option (global only);
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;
Sun, 30 Jun 2013 11:37:34 +0200 wenzelm backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
Thu, 27 Jun 2013 23:17:26 +0200 wenzelm manage option "proofs" within theory context -- with minor overhead for primitive inferences;
Wed, 29 May 2013 18:25:11 +0200 wenzelm tuned signature -- more explicit flags for low-level Thm.bicompose;
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;
Fri, 24 May 2013 17:00:46 +0200 wenzelm tuned signature;
Wed, 03 Apr 2013 20:56:08 +0200 wenzelm updated comment to 46b90bbc370d;
Fri, 30 Nov 2012 22:38:06 +0100 wenzelm print formal entities with markup;
Mon, 19 Nov 2012 20:23:47 +0100 wenzelm theorem status about oracles/futures is no longer printed by default;
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);
Sun, 15 Jul 2012 17:53:47 +0200 wenzelm prefer canonical fold_rev;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
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;
Tue, 14 Feb 2012 22:22:01 +0100 wenzelm tuned signature;
Wed, 25 Jan 2012 14:13:59 +0100 wenzelm removed obscure/outdated material;
Sat, 14 Jan 2012 20:05:58 +0100 wenzelm renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
Sat, 14 Jan 2012 19:06:05 +0100 wenzelm renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
Thu, 10 Nov 2011 17:41:36 +0100 wenzelm discontinued unused Thm.compress (again);
Thu, 03 Nov 2011 22:51:37 +0100 wenzelm tuned signature;
less more (0) -300 -100 -60 tip