2011-04-18 ago pass plain Proof.context for pretty printing;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2010-12-17 ago renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
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-05 ago turned show_sorts/show_types into proper configuration options;
2010-09-05 ago pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-08-11 ago tuned whitespace
2010-06-01 ago avoid store flag in add_* operations
2010-06-01 ago do not expose store flag of AxClass.add_*
2010-06-01 ago classrel and arity theorems are now stored under proper name in theory. add_arity and
2010-05-15 ago eliminated redundant runtime checks;
2010-05-15 ago normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
2010-05-13 ago the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
2010-05-09 ago just one version of Thm.unconstrainT, which affects all variables;
2010-05-08 ago back-patching of axclass proofs;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 ago made SML/NJ happy;
2010-04-27 ago removed obsolete sanity check -- Sign.certify_sort is stable;
2010-04-27 ago tuned signature;
2010-04-27 ago tuned classrel completion -- bypass composition with reflexive edges;
2010-04-27 ago tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
2010-04-27 ago tuned aritiy completion -- slightly less intermediate data structures;
2010-04-27 ago clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
2010-04-27 ago misc tuning and simplification;
2010-04-26 ago removed unused AxClass.class_intros;
2010-04-25 ago renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
2010-04-25 ago more systematic treatment of data -- avoid slightly odd nested tuples here;
2010-04-25 ago replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-25 ago misc tuning and simplification;
2010-04-25 ago simplified some private bindings;
2010-04-25 ago classrel and arity completion by krauss/schropp;
2010-04-11 ago Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-25 ago Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
2010-03-25 ago removed unused AxClass.of_sort derivation;
2010-03-22 ago inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;
2010-03-22 ago replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-21 ago Logic.mk_of_sort convenience;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-09 ago added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
2010-02-19 ago Thm.def_binding;
2010-02-18 ago axclass: more precise treatment of naming vs. binding;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-01-04 ago discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
2010-01-04 ago dropped copy operation for legacy TheoryDataFun
2009-11-30 ago dropped some unused bindings
2009-10-29 ago eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
2009-10-28 ago conceal internal bindings;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 ago maintain theory name via name space, not tags;
2009-10-22 ago explicit close_derivation
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-09-30 ago removed dead code;
2009-09-29 ago modernized Balanced_Tree;
2009-07-26 ago Goal.finish: explicit context for printing;
2009-07-07 ago add_classrel/arity: strip_shyps of stored result;
2009-07-06 ago clarified Thm.of_class/of_sort/class_triv;
2009-07-06 ago renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-02 ago renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);