src/Pure/global_theory.ML
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 Position.here;
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;