src/Pure/facts.ML
Mon, 04 Jul 2016 11:11:19 +0200 wenzelm tuned signature;
Tue, 21 Jun 2016 14:42:47 +0200 wenzelm position information for literal facts;
Tue, 07 Jun 2016 21:13:08 +0200 wenzelm clarified signature;
Tue, 10 May 2016 22:25:06 +0200 wenzelm find dynamic facts as well, but static ones are preferred;
Sun, 30 Aug 2015 17:34:29 +0200 wenzelm trim context for persistent storage;
Thu, 13 Aug 2015 11:05:19 +0200 wenzelm tuned signature, in accordance to sortBy in Scala;
Tue, 31 Mar 2015 20:18:10 +0200 wenzelm tuned signature;
Tue, 31 Mar 2015 20:07:37 +0200 wenzelm tuned signature;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Thu, 14 Aug 2014 16:20:14 +0200 wenzelm more informative Token.Fact: retain name of dynamic fact (without selection);
Sun, 10 Aug 2014 19:44:20 +0200 wenzelm support aliases within the facts space;
Sat, 15 Mar 2014 11:22:25 +0100 wenzelm more explicit treatment of verbose mode, which includes concealed entries;
Fri, 14 Mar 2014 10:08:36 +0100 wenzelm just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
Thu, 13 Mar 2014 12:28:35 +0100 wenzelm minor tuning -- NB: props are usually empty for global facts;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Sun, 09 Mar 2014 17:07:45 +0100 wenzelm removed dead code;
Sun, 09 Mar 2014 17:02:18 +0100 wenzelm check fact names with PIDE markup;
Tue, 25 Feb 2014 11:36:04 +0100 wenzelm more positions;
Wed, 17 Oct 2012 10:45:43 +0200 wenzelm tuned signature;
Tue, 09 Oct 2012 19:24:19 +0200 wenzelm more explicit flags for facts table;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Sun, 25 Oct 2009 19:14:25 +0100 wenzelm export is_concealed;
Sat, 24 Oct 2009 20:54:08 +0200 wenzelm maintain explicit name space kind;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Sat, 24 Oct 2009 19:22:39 +0200 wenzelm eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
Mon, 09 Feb 2009 17:25:07 +1100 Timothy Bourke Nicer names in FindTheorems.
Wed, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Mon, 01 Dec 2008 19:41:16 +0100 haftmann new Binding module
Thu, 20 Nov 2008 19:06:03 +0100 haftmann fact table now using name bindings
Tue, 05 Aug 2008 13:31:31 +0200 wenzelm Facts.lookup: return static/dynamic status;
Thu, 12 Jun 2008 16:41:57 +0200 wenzelm dest/export_static: content difference;
Wed, 16 Apr 2008 21:53:00 +0200 wenzelm removed unused space_of;
Tue, 15 Apr 2008 18:49:18 +0200 wenzelm renamed dest to dest_table, and extern to extern table;
Tue, 15 Apr 2008 16:12:11 +0200 wenzelm disallow duplicate entries (weak version for merge);
Tue, 25 Mar 2008 19:39:59 +0100 wenzelm support dynamic facts;
Thu, 20 Mar 2008 17:38:53 +0100 wenzelm added pos_of_ref;
Thu, 20 Mar 2008 16:04:30 +0100 wenzelm Facts.Named: include position;
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Mon, 17 Mar 2008 20:51:09 +0100 wenzelm replaced generic add by add_local/add_global;
Sat, 15 Mar 2008 22:07:31 +0100 wenzelm del: hide in name space;
Sat, 15 Mar 2008 18:08:02 +0100 wenzelm Environment of named facts (admits overriding). Optional indexing by proposition.
less more (0) tip