src/Pure/Isar/proof_context.ML
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2009-01-02 wenzelm 2009-01-02 added numeral, which supercedes num, xnum, float; renamed xstr to inner_string;
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
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-11-20 haftmann 2008-11-20 using name bindings
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-11-14 haftmann 2008-11-14 namify and name_decl combinators
2008-09-29 wenzelm 2008-09-29 put_thms: ContextPosition.set_visible false;
2008-09-29 wenzelm 2008-09-29 back to plain Position.report for regular references; ContextPosition.report_visible for decls; report_token/parse_token: back to context-less version;
2008-09-29 wenzelm 2008-09-29 ContextPosition.report; parse_token/report_token: explicit context;
2008-09-29 wenzelm 2008-09-29 added norm_export_morphism;
2008-09-12 wenzelm 2008-09-12 added extern_fact (local or global); more procise printing of fact names;
2008-09-12 wenzelm 2008-09-12 pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
2008-09-02 wenzelm 2008-09-02 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 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements; report local_fact_decl, fixed_decl; simplified ProofContext.inferred_param;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-08-14 wenzelm 2008-08-14 retrieve_thms: transfer fact position to result; tuned;
2008-08-11 wenzelm 2008-08-11 renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
2008-08-10 wenzelm 2008-08-10 read_tyname/const/const_proper: report position; moved parse_token to syntax.ML; tuned;
2008-08-07 wenzelm 2008-08-07 parse_token: use Syntax.read_token, pass full position information;
2008-08-06 wenzelm 2008-08-06 parse_sort/typ/term/prop: report markup;
2008-08-05 wenzelm 2008-08-05 Facts.lookup: return static/dynamic status;
2008-06-21 wenzelm 2008-06-21 added query_type/const/class (meta data);
2008-06-19 wenzelm 2008-06-19 renamed is_abbrev_mode to abbrev_mode; added private get_sort (from sign.ML);
2008-06-18 wenzelm 2008-06-18 simplified TypeInfer.infer_types;
2008-06-18 wenzelm 2008-06-18 export transfer_syntax; added allow_dummies feature (for legacy emulations); moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
2008-06-13 wenzelm 2008-06-13 map_const: soft version, no failure here;
2008-06-12 wenzelm 2008-06-12 Facts.dest/export_static: content difference;
2008-05-18 wenzelm 2008-05-18 unparse_term: check PureThy.old_appl_syntax instead of CPure;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 default token translations: observe Sign.is_pretty_global for fixed variables;
2008-04-22 haftmann 2008-04-22 exported is_abbrev mode discriminator
2008-04-18 wenzelm 2008-04-18 print_cases: proper context for revert_skolem;
2008-04-17 wenzelm 2008-04-17 revert_skolem: do not change non-reversible names; default token translations: revert_skolem; removed obsolete revert_skolems;
2008-04-17 wenzelm 2008-04-17 default token translations with proper markup;
2008-04-16 wenzelm 2008-04-16 Facts.extern_static;
2008-04-16 wenzelm 2008-04-16 removed obsolete valid_thms; removed obsolete premsN binding; PureThy.get_fact: pass dynamic context;
2008-04-15 wenzelm 2008-04-15 Facts.intern, Facts.extern_table;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-25 wenzelm 2008-03-25 support dynamic facts;
2008-03-20 wenzelm 2008-03-20 Facts.Named: include position;
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument; renamed former get_thm to get_fact_single, and get_thms to get_fact;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-18 wenzelm 2008-03-18 valid_thms: get_thms_silent;
2008-03-17 wenzelm 2008-03-17 Facts.add_local;
2008-03-15 wenzelm 2008-03-15 replaced obsolete FactIndex.T by Facts.T; removed unused get_thm(s)_closure; removed obsolete theorems_of, fact_index_of, lthms_containing, hide_thms;
2008-03-14 haftmann 2008-03-14 added mk_const functions
2008-03-11 wenzelm 2008-03-11 put_thms: pass do_props;
2008-03-07 haftmann 2008-03-07 dropped local tsigs
2008-03-05 wenzelm 2008-03-05 put_thms: do not index facts here (affects prems/this/calculation in particular);
2007-11-27 wenzelm 2007-11-27 standard_parse_term: check ambiguous results without changing the result yet;
2007-11-23 haftmann 2007-11-23 explicit type signature
2007-11-21 wenzelm 2007-11-21 intern_skolem: disallow qualified names;
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest; export standard_infer_types;
2007-11-08 wenzelm 2007-11-08 removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy; discontinued legacy_intern_skolem, gen_read';