src/Pure/more_thm.ML
Wed, 25 Apr 2018 14:13:44 +0200 wenzelm tuned -- avoid spurious exception trace for "the";
Wed, 07 Mar 2018 17:27:57 +0100 wenzelm eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;
Sun, 25 Feb 2018 19:43:38 +0100 wenzelm prefer symbols;
Sun, 25 Feb 2018 15:44:46 +0100 wenzelm eliminated ASCII syntax from Pure bootstrap;
Wed, 21 Feb 2018 18:41:41 +0100 wenzelm explicit operations to instantiate frees: typ, term, thm, morphism;
Mon, 19 Feb 2018 22:07:21 +0100 wenzelm support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
Sun, 18 Feb 2018 15:05:21 +0100 wenzelm tuned signature;
Thu, 01 Feb 2018 13:55:10 +0100 wenzelm clarified signature;
Thu, 22 Jun 2017 21:10:13 +0200 wenzelm consolidate proofs more simultaneously;
Mon, 10 Apr 2017 21:05:31 +0200 wenzelm tuned signature;
Fri, 16 Dec 2016 19:07:16 +0100 wenzelm consolidate nested thms with persistent result, for improved performance;
Wed, 14 Dec 2016 18:22:18 +0100 wenzelm more careful derivation_closed / close_derivation;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Thu, 23 Jun 2016 11:01:14 +0200 wenzelm tuned signature;
Mon, 25 Apr 2016 16:54:48 +0200 wenzelm clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
Thu, 07 Jan 2016 15:53:39 +0100 wenzelm more uniform treatment of package internals;
Wed, 16 Dec 2015 16:31:36 +0100 wenzelm rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
Tue, 15 Dec 2015 16:57:10 +0100 wenzelm tuned signature -- clarified modules;
Fri, 23 Oct 2015 17:30:18 +0200 wenzelm print thm wrt. local shyps (from full proof context);
Fri, 23 Oct 2015 17:17:11 +0200 wenzelm clarified modules;
Tue, 06 Oct 2015 16:57:14 +0200 wenzelm added Thm.forall_intr_name;
Tue, 06 Oct 2015 13:31:44 +0200 wenzelm just one theorem kind, which is legacy anyway;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Fri, 25 Sep 2015 19:20:24 +0200 wenzelm tuned;
Fri, 25 Sep 2015 19:13:47 +0200 wenzelm tuned signature: eliminated pointless type Context.pretty;
Thu, 24 Sep 2015 23:33:29 +0200 wenzelm more explicit Defs.context: use proper name spaces as far as possible;
Sun, 30 Aug 2015 22:58:26 +0200 wenzelm trim context for persistent storage;
Fri, 28 Aug 2015 13:36:33 +0200 wenzelm tuned;
Fri, 28 Aug 2015 13:23:02 +0200 wenzelm tuned;
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:44:21 +0200 wenzelm tuned;
Sun, 16 Aug 2015 18:19:30 +0200 wenzelm prefer theory_id operations;
Sat, 15 Aug 2015 20:07:05 +0200 wenzelm clarified context;
Tue, 28 Jul 2015 21:47:03 +0200 wenzelm more explicit context;
Tue, 28 Jul 2015 21:31:16 +0200 wenzelm eliminated dead code;
Tue, 28 Jul 2015 20:15:19 +0200 wenzelm more direct access to atomic cterms;
Tue, 28 Jul 2015 20:05:53 +0200 wenzelm proper context;
Tue, 28 Jul 2015 19:49:54 +0200 wenzelm more direct access to atomic cterms;
Tue, 28 Jul 2015 18:59:15 +0200 wenzelm clarified context;
Mon, 27 Jul 2015 23:40:39 +0200 wenzelm tuned signature;
Mon, 27 Jul 2015 17:44:55 +0200 wenzelm tuned signature;
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);
Wed, 03 Jun 2015 19:25:05 +0200 wenzelm clarified context;
Mon, 01 Jun 2015 10:47:08 +0200 wenzelm tuned;
Wed, 08 Apr 2015 16:24:22 +0200 wenzelm explicitly checked alpha conversion -- actual renaming happens outside kernel;
Fri, 06 Mar 2015 17:32:20 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Thu, 05 Mar 2015 13:28:04 +0100 wenzelm tuned -- more explicit use of context;
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};
Mon, 18 Aug 2014 15:46:27 +0200 wenzelm more general dummy: may contain "parked arguments", for example;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Thu, 20 Feb 2014 20:59:15 +0100 wenzelm clarified printing of undeclared hyps;
Mon, 17 Feb 2014 22:39:20 +0100 wenzelm subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
Sat, 11 Jan 2014 23:53:38 +0100 wenzelm check_hyps when attributes are applied;
Sat, 11 Jan 2014 20:06:31 +0100 wenzelm check_hyps for attribute application (still inactive, due to non-compliant tools);
Fri, 10 Jan 2014 21:37:28 +0100 wenzelm more elementary management of declared hyps, below structure Assumption;
less more (0) -100 -60 tip