17 months ago ago disallow pending hyps;
18 months ago ago more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
21 months ago ago tuned -- more uniform;
21 months ago ago tuned signature;
21 months ago ago tuned signature;
21 months ago ago tuned;
21 months ago ago support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
21 months ago ago tuned: more accurate transfer;
21 months ago ago store facts as lazy values;
2017-04-10 ago tuned signature;
2016-01-13 ago tuned;
2016-01-13 ago removed old 'defs' command;
2015-09-25 ago tuned signature: eliminated pointless type Context.pretty;
2015-09-24 ago more explicit Defs.context: use proper name spaces as far as possible;
2015-08-30 ago trim context for persistent storage;
2014-08-14 ago more informative Token.Fact: retain name of dynamic fact (without selection);
2014-08-13 ago tuned signature -- proper Local_Theory.add_thms_dynamic;
2014-08-10 ago support aliases within the facts space;
2014-03-15 ago tuned signature;
2014-03-14 ago just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
2014-03-09 ago check fact names with PIDE markup;
2014-02-25 ago more positions;
2013-07-30 ago type theory is purely value-oriented;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-09 ago more explicit flags for facts table;
2012-09-01 ago discontinued complicated/unreliable notion of recent proofs within context;
2012-08-31 ago tuned signature;
2012-08-30 ago some support for registering forked proofs within Proof.state, using its bottom context;
2012-08-30 ago tuned signature;
2012-08-29 ago renamed Position.str_of to;
2012-04-04 ago tuned comments;
2012-03-18 ago tuned;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-03 ago canonical argument order for attribute application;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-26 ago memoing of forked proofs;
2011-08-19 ago maintain recent future proofs at transaction boundaries;
2011-04-23 ago hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
2011-04-17 ago added Binding.print convenience, which includes quote already;
2011-04-17 ago tuned signature;
2011-04-17 ago markup facts via name space;
2011-04-17 ago eliminated obsolete markup -- superseded by generic "entity" markup;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-02-02 ago tuned odd conditional expression;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;