2014-03-15 wenzelm 2014-03-15 tuned signature; eliminated clones;
2014-03-14 wenzelm 2014-03-14 just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.); more thorough background_notes: distribute global notes to all contexts;
2014-03-09 wenzelm 2014-03-09 check fact names with PIDE markup;
2014-02-25 wenzelm 2014-02-25 more positions; tuned messages;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-09 wenzelm 2012-10-09 more explicit flags for facts table;
2012-09-01 wenzelm 2012-09-01 discontinued complicated/unreliable notion of recent proofs within context;
2012-08-31 wenzelm 2012-08-31 tuned signature;
2012-08-30 wenzelm 2012-08-30 some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
2012-08-30 wenzelm 2012-08-30 tuned signature;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to;
2012-04-04 wenzelm 2012-04-04 tuned comments;
2012-03-18 wenzelm 2012-03-18 tuned;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-03-03 wenzelm 2012-03-03 canonical argument order for attribute application;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-26 wenzelm 2011-11-26 memoing of forked proofs;
2011-08-19 wenzelm 2011-08-19 maintain recent future proofs at transaction boundaries;
2011-04-23 wenzelm 2011-04-23 hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-17 wenzelm 2011-04-17 tuned signature;
2011-04-17 wenzelm 2011-04-17 markup facts via name space; eliminated obsolete markup;
2011-04-17 wenzelm 2011-04-17 eliminated obsolete markup -- superseded by generic "entity" markup;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-02-02 wenzelm 2011-02-02 tuned odd conditional expression;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;