src/Pure/Isar/proof_context.ML
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 ago simplified some internal flags using Config.T instead of full-blown Proof_Data;
2010-09-17 ago tuned signature of (Context_)Position.report variants;
2010-09-17 ago allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
2010-09-13 ago tuned signature;
2010-09-13 ago Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
2010-09-12 ago Type_Infer.infer_types: plain error instead of kernel exception TYPE;
2010-09-12 ago load type_infer.ML later -- proper context for Type_Infer.infer_types;
2010-09-12 ago eliminated aliases of Type.constraint;
2010-09-07 ago highlight bad range of nested error (here from inner parsing);
2010-09-06 ago discontinued obsolete ProofContext.prems_limit;
2010-09-05 ago Syntax.standard_parse_term: eliminated redundant Pretty.pp;
2010-09-02 ago inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;
2010-09-02 ago turned show_question_marks into proper configuration option;
2010-09-01 ago prefer regular print functions over slightly low-level Term.string_of_vname;
2010-08-26 ago renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-11 ago tuned whitespace;
2010-08-08 ago proper context for Syntax.parse_token;
2010-08-08 ago prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-29 ago read_const: disallow internal names as usual in visible Isar text;
2010-04-29 ago ProofContext.read_const: allow for type constraint (for fixed variable);
2010-04-29 ago allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;
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;