22 months ago wenzelm 2018-07-28 eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;
2018-02-20 wenzelm 2018-02-20 avoid premature Lazy.force due to strict "?" operator;
2018-02-19 wenzelm 2018-02-19 clarified modules;
2018-02-19 wenzelm 2018-02-19 store facts as lazy values;
2018-02-18 wenzelm 2018-02-18 tuned signature;
2016-07-04 wenzelm 2016-07-04 tuned signature;
2016-06-21 wenzelm 2016-06-21 position information for literal facts; Markup.entry may have empty kind/name;
2016-06-07 wenzelm 2016-06-07 clarified signature;
2016-05-10 wenzelm 2016-05-10 find dynamic facts as well, but static ones are preferred; tuned;
2015-08-30 wenzelm 2015-08-30 trim context for persistent storage;
2015-08-13 wenzelm 2015-08-13 tuned signature, in accordance to sortBy in Scala;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-08-14 wenzelm 2014-08-14 more informative Token.Fact: retain name of dynamic fact (without selection);
2014-08-10 wenzelm 2014-08-10 support aliases within the facts space;
2014-03-15 wenzelm 2014-03-15 more explicit treatment of verbose mode, which includes concealed entries;
2014-03-14 wenzelm 2014-03-14 just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.); more thorough background_notes: distribute global notes to all contexts;
2014-03-13 wenzelm 2014-03-13 minor tuning -- NB: props are usually empty for global facts;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2014-03-09 wenzelm 2014-03-09 removed dead code;
2014-03-09 wenzelm 2014-03-09 check fact names with PIDE markup;
2014-02-25 wenzelm 2014-02-25 more positions; tuned messages;
2012-10-17 wenzelm 2012-10-17 tuned signature; prefer exception Fail for internal errors;
2012-10-09 wenzelm 2012-10-09 more explicit flags for facts table;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-10-25 wenzelm 2009-10-25 export is_concealed; tuned;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; fully authentic merge;
2009-02-09 Timothy Bourke 2009-02-09 Nicer names in FindTheorems. * Patch NameSpace.get_accesses, contributed by Timothy Bourke: NameSpace.get_accesses has been patched to fix the following bug: theory OverHOL imports Main begin lemma conjI: "a & b --> b" by blast ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of; val x1 = NameSpace.get_accesses ns "HOL.conjI"; val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *} end where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"], but x1 should be just ["HOL.conjI"]. NameSpace.get_accesses is only used within the NameSpace structure itself. The two uses have been modified to retain their original behaviour. Note that NameSpace.valid_accesses gives different results: get_accesses ns "HOL.eq_class.eq" gives ["eq", "eq_class.eq", "HOL.eq_class.eq"] but, valid_accesses ns "HOL.eq_class.eq" gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"] * Patch FindTheorems: Prefer names that are shorter to type in the current context. * Re-export space_of.
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-01 haftmann 2008-12-01 new Binding module
2008-11-20 haftmann 2008-11-20 fact table now using name bindings
2008-08-05 wenzelm 2008-08-05 Facts.lookup: return static/dynamic status;
2008-06-12 wenzelm 2008-06-12 dest/export_static: content difference; tuned comments;
2008-04-16 wenzelm 2008-04-16 removed unused space_of; added defined, fold_static; renamed dest_table to dest_static; renamed extern_table to extern_static;
2008-04-15 wenzelm 2008-04-15 renamed dest to dest_table, and extern to extern table; added name space intern/extern;
2008-04-15 wenzelm 2008-04-15 disallow duplicate entries (weak version for merge); added hide;
2008-03-25 wenzelm 2008-03-25 support dynamic facts;
2008-03-20 wenzelm 2008-03-20 added pos_of_ref;
2008-03-20 wenzelm 2008-03-20 Facts.Named: include position;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-17 wenzelm 2008-03-17 replaced generic add by add_local/add_global; add_global: report/ignore duplicate bindings;
2008-03-15 wenzelm 2008-03-15 del: hide in name space;
2008-03-15 wenzelm 2008-03-15 Environment of named facts (admits overriding). Optional indexing by proposition.