src/Pure/context.ML
Sat, 06 Dec 2008 00:08:07 +0100 wenzelm finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
Thu, 16 Oct 2008 22:44:26 +0200 wenzelm tuned;
Fri, 26 Sep 2008 19:07:56 +0200 wenzelm eliminated polymorphic equality;
Mon, 22 Sep 2008 15:26:11 +0200 wenzelm added reject_draft;
Thu, 04 Sep 2008 16:03:44 +0200 wenzelm Thread.getLocal/setLocal;
Tue, 24 Jun 2008 19:43:17 +0200 wenzelm added pprint_thy_ref;
Sun, 18 May 2008 17:03:20 +0200 wenzelm eliminated theory CPure;
Wed, 14 May 2008 14:43:37 +0200 wenzelm names_of: exclude intermediate ids -- less verbosity;
Thu, 10 Apr 2008 20:54:15 +0200 wenzelm export is_draft, not draftN;
Sat, 29 Mar 2008 19:14:08 +0100 wenzelm added map_theory_result, map_proof_result;
Fri, 28 Mar 2008 20:02:04 +0100 wenzelm Context.>> : operate on Context.generic;
Thu, 27 Mar 2008 15:32:15 +0100 wenzelm eliminated delayed theory setup
Thu, 27 Mar 2008 14:41:14 +0100 wenzelm eliminated theory ProtoPure;
Thu, 27 Mar 2008 12:06:26 +0100 wenzelm nonfix >>;
Wed, 26 Mar 2008 22:40:03 +0100 wenzelm added thread data (formerly global ref in ML/ml_context.ML);
Sat, 08 Sep 2007 19:58:35 +0200 wenzelm removed thy_ord (erratic due to multi-threading);
Mon, 20 Aug 2007 23:41:35 +0200 wenzelm tuned CRITICAL sections;
Wed, 08 Aug 2007 16:40:20 +0200 wenzelm thread-safeness: when creating certified items, perform Theory.check_thy *last*;
Fri, 03 Aug 2007 16:28:20 +0200 wenzelm improved check_thy: produce a checked theory_ref (thread-safe version);
Mon, 23 Jul 2007 20:47:56 +0200 wenzelm marked some CRITICAL sections;
Thu, 05 Jul 2007 20:01:32 +0200 wenzelm the_theory/proof: error instead of exception Fail;
Wed, 13 Jun 2007 00:01:58 +0200 wenzelm merge/merge_refs: plain error instead of exception TERM;
Mon, 07 May 2007 00:50:09 +0200 wenzelm simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
Mon, 30 Apr 2007 13:33:00 +0200 wenzelm removed obsolete get_sg;
Thu, 05 Apr 2007 00:30:31 +0200 wenzelm added thy_ord -- order of creation;
Wed, 04 Apr 2007 23:29:39 +0200 wenzelm theory: maintain ancestors in order of creation;
Sun, 21 Jan 2007 16:46:06 +0100 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
Sun, 21 Jan 2007 16:43:47 +0100 wenzelm tuned comments
Sat, 20 Jan 2007 14:09:16 +0100 wenzelm added is_finished_thy;
Fri, 19 Jan 2007 22:08:02 +0100 wenzelm moved ML context stuff to from Context to ML_Context;
Fri, 19 Jan 2007 13:09:32 +0100 wenzelm ML context: full generic context, tuned signature;
Sat, 30 Dec 2006 16:08:00 +0100 wenzelm removed conditional combinator;
Tue, 05 Dec 2006 22:14:45 +0100 wenzelm added mapping_result;
Fri, 24 Nov 2006 22:05:14 +0100 wenzelm fake predeclaration of structure ProofContext;
Mon, 09 Oct 2006 19:37:05 +0200 wenzelm moved Context.ml_output to Output.ml_output;
Sun, 01 Oct 2006 22:19:24 +0200 wenzelm exists_name: include this theory name;
Wed, 02 Aug 2006 22:26:51 +0200 wenzelm fake predeclaration of type Proof.context;
Wed, 07 Jun 2006 16:53:31 +0200 haftmann fixed typo
Wed, 17 May 2006 22:34:47 +0200 wenzelm added mapping;
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Wed, 15 Feb 2006 21:34:55 +0100 wenzelm removed distinct, renamed gen_distinct to distinct;
Sun, 12 Feb 2006 21:34:22 +0100 wenzelm structure Datatab: private copy avoids potential conflict of table exceptions;
Mon, 06 Feb 2006 20:58:57 +0100 wenzelm TableFun: renamed xxx_multi to xxx_list;
Sat, 21 Jan 2006 23:02:23 +0100 wenzelm rename map_theory/proof to theory/proof_map;
Thu, 19 Jan 2006 21:22:16 +0100 wenzelm setup: theory -> theory;
Sat, 14 Jan 2006 17:14:06 +0100 wenzelm sane ERROR handling;
Fri, 13 Jan 2006 01:13:02 +0100 wenzelm added map_theory, map_proof;
Tue, 10 Jan 2006 19:33:31 +0100 wenzelm support for generic contexts with data;
Tue, 04 Oct 2005 19:01:37 +0200 wenzelm minor tweaks for Poplog/ML;
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Tue, 13 Sep 2005 22:19:24 +0200 wenzelm replaced DATA_FAIL by EXCEPTION;
Thu, 01 Sep 2005 18:48:50 +0200 wenzelm curried_lookup/update;
Tue, 16 Aug 2005 13:42:31 +0200 wenzelm type proof: theory_ref instead of theory (make proof contexts independent entities);
Tue, 19 Jul 2005 20:47:01 +0200 wenzelm Inttab.defined;
Wed, 06 Jul 2005 20:00:24 +0200 wenzelm check_thy: less invocations, less verbose;
Wed, 29 Jun 2005 15:13:23 +0200 wenzelm added joinable;
Wed, 22 Jun 2005 19:41:18 +0200 wenzelm begin_thy: merge maximal imports;
Mon, 20 Jun 2005 22:14:03 +0200 wenzelm improved treatment of intermediate checkpoints: actual copy
Fri, 17 Jun 2005 18:33:21 +0200 wenzelm added type theory: generic theory contexts with unique identity,
Thu, 21 Apr 2005 22:02:06 +0200 wenzelm superceded by Pure.thy and CPure.thy;
less more (0) -60 tip