src/Pure/Isar/proof_context.ML
2010-04-28 ago localized default sort;
2010-04-28 ago more systematic naming of tsig operations;
2010-04-28 ago get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred);
2010-04-27 ago monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-15 ago get_sort: suppress dummyS from input;
2010-03-09 ago aliases for class/type/const;
2010-03-09 ago added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
2010-03-06 ago provide ProofContext.def_type depending on "pattern" mode;
2010-03-03 ago authentic syntax for classes and type constructors;
2010-03-01 ago more uniform treatment of syntax for types vs. consts;
2010-02-27 ago clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2010-02-25 ago clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-02-21 ago slightly more abstract syntax mark/unmark operations;
2010-02-21 ago authentic syntax for *all* term constants;
2010-02-18 ago Use top-down rewriting to contract abbreviations.
2010-02-16 ago simplified meaning of ProofContext.verbose;
2010-02-16 ago misc tuning and simplification;
2010-02-15 ago discontinued unnamed infix syntax;
2010-02-11 ago added ML antiquotation @{syntax_const};
2010-02-02 ago added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-15 ago eliminated obsolete thm position tags;
2009-11-12 ago eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
2009-11-09 ago locale_const/target_notation: uniform use of Term.aconv_untyped;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-11-02 ago modernized structure Local_Syntax;
2009-11-02 ago modernized structure AutoBind;
2009-11-02 ago modernized structure Context_Position;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-27 ago ProofContext.setmp_verbose_CRITICAL;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 ago more direct access to naming;
2009-10-25 ago allow name space entries to be "concealed" -- via binding/naming/local_theory;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-20 ago backpatching of structure Proof and ProofContext -- avoid odd aliases;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-09-30 ago eliminated redundant bindings;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-21 ago moved ProofContext.pretty_thm to Display.pretty_thm etc.;
2009-07-17 ago tuned/modernized Envir operations;
2009-07-14 ago tuned prepare_patternT: Term.exists_subtype;
2009-03-31 ago tuned error message;
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 ago renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 ago tuned;
2009-03-28 ago replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-26 ago pretty_thm_aux etc.: explicit show_status flag;
2009-03-21 ago removed obsolete pprint operations;
2009-03-19 ago use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-18 ago de-camelized Symbol_Pos;
2009-03-17 ago reverted abbreviations: improved performance via Item_Net.T;
2009-03-12 ago Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-12 ago renamed sticky_prefix to mandatory_path;
2009-03-11 ago eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
2009-03-10 ago Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
2009-03-10 ago removed obsolete no_base_names;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
2009-03-05 ago eliminated obsolete ProofContext.full_bname;