2012-04-27 ago clarified signature;
2012-04-01 ago added Attrib.global_notes/local_notes/generic_notes convenience;
2012-03-13 ago refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
2012-03-13 ago tuned;
2012-03-10 ago tuned;
2012-02-28 ago display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2011-11-20 ago tuned signature;
2011-11-19 ago do not store vacuous theorem specifications -- relevant for frugal local theory content;
2011-11-07 ago tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-05 ago more uniform instT_subst vs. inst_subst: compare variable names only;
2011-11-05 ago some performance tuning via Term_Subst/Same.operation;
2011-11-05 ago pruned signature;
2011-11-03 ago tuned whitespace;
2011-10-29 ago tuned;
2011-10-28 ago tuned signature -- refined terminology;
2011-10-28 ago slightly more explicit/syntactic modelling of morphisms;
2011-08-08 ago misc tuning -- eliminated old-fashioned rep_thm;
2011-07-15 ago Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);
2011-07-15 ago do not check vacous bindings, which routinely occur in locale expressions and long theorem statements etc.;
2011-06-25 ago clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
2011-04-27 ago clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-27 ago tuned signature -- eliminated odd comment;
2011-04-27 ago reorganized fixes as specialized (global) name space;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago tuned signature, disentangled dependencies;
2011-04-08 ago discontinued special treatment of structure Mixfix;
2011-01-15 ago clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
2011-01-03 ago tuned whitespace
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-06 ago turned show_hyps and show_tags into proper configuration option;
2010-08-25 ago structure Thm: less pervasive names;
2010-07-31 ago Interpretation in proofs supports mixins.
2010-05-05 ago eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-03-13 ago removed unused Args.maxidx_values and Element.generalize_facts;
2010-03-07 ago modernized structure Object_Logic;
2010-03-07 ago modernized structure Local_Defs;
2009-11-02 ago modernized structure Proof_Display;
2009-07-26 ago Variable.focus: named parameters;
2009-07-25 ago Method.Basic: no position;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-03-29 ago simplified Element.activate(_i): singleton version;
2009-03-29 ago added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 ago renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-19 ago use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-11 ago eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
2009-03-11 ago Thm.def_binding_optional;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-03-03 ago Binding.str_of;
2009-03-03 ago Thm.binding;
2009-01-21 ago eliminated obsolete var morphism;
2009-01-21 ago refined witness algebra