src/Pure/Isar/proof_context.ML
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-03-03 ago Binding.str_of;
2009-03-03 ago Thm.binding;
2009-03-01 ago use long names for old-style fold combinators;
2009-01-21 ago removed Ids;
2009-01-21 ago binding is alias for Binding.T
2009-01-02 ago added numeral, which supercedes num, xnum, float;
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-12-01 ago new Binding module
2008-11-20 ago fact table now using name bindings
2008-11-20 ago using name bindings
2008-11-20 ago Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-11-14 ago namify and name_decl combinators
2008-09-29 ago put_thms: ContextPosition.set_visible false;
2008-09-29 ago back to plain Position.report for regular references;
2008-09-29 ago ContextPosition.report;
2008-09-29 ago added norm_export_morphism;
2008-09-12 ago added extern_fact (local or global);
2008-09-12 ago pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
2008-09-02 ago pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-27 ago type Properties.T;
2008-08-14 ago retrieve_thms: transfer fact position to result;
2008-08-11 ago renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
2008-08-10 ago read_tyname/const/const_proper: report position;
2008-08-07 ago parse_token: use Syntax.read_token, pass full position information;
2008-08-06 ago parse_sort/typ/term/prop: report markup;
2008-08-05 ago Facts.lookup: return static/dynamic status;
2008-06-21 ago added query_type/const/class (meta data);
2008-06-19 ago renamed is_abbrev_mode to abbrev_mode;
2008-06-18 ago simplified TypeInfer.infer_types;
2008-06-18 ago export transfer_syntax;
2008-06-13 ago map_const: soft version, no failure here;
2008-06-12 ago Facts.dest/export_static: content difference;
2008-05-18 ago unparse_term: check PureThy.old_appl_syntax instead of CPure;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago default token translations: observe Sign.is_pretty_global for fixed variables;
2008-04-22 ago exported is_abbrev mode discriminator
2008-04-18 ago print_cases: proper context for revert_skolem;
2008-04-17 ago revert_skolem: do not change non-reversible names;
2008-04-17 ago default token translations with proper markup;
2008-04-16 ago Facts.extern_static;
2008-04-16 ago removed obsolete valid_thms;
2008-04-15 ago Facts.intern, Facts.extern_table;
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2008-03-25 ago support dynamic facts;
2008-03-20 ago Facts.Named: include position;
2008-03-20 ago simplified get_thm(s): back to plain name argument;
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-18 ago valid_thms: get_thms_silent;
2008-03-17 ago Facts.add_local;
2008-03-15 ago replaced obsolete FactIndex.T by Facts.T;
2008-03-14 ago added mk_const functions
2008-03-11 ago put_thms: pass do_props;
2008-03-07 ago dropped local tsigs
2008-03-05 ago put_thms: do not index facts here (affects prems/this/calculation in particular);