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;