src/Pure/facts.ML
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.