2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-01-15 wenzelm 2011-01-15 clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
2011-01-03 haftmann 2011-01-03 tuned whitespace
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
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;
2010-09-06 wenzelm 2010-09-06 turned show_hyps and show_tags into proper configuration option;
2010-08-25 wenzelm 2010-08-25 structure Thm: less pervasive names;
2010-07-31 ballarin 2010-07-31 Interpretation in proofs supports mixins.
2010-05-05 haftmann 2010-05-05 eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-03-13 wenzelm 2010-03-13 removed unused Args.maxidx_values and Element.generalize_facts;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Display;
2009-07-26 wenzelm 2009-07-26 Variable.focus: named parameters;
2009-07-25 wenzelm 2009-07-25 Method.Basic: no position;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-03-29 wenzelm 2009-03-29 simplified Element.activate(_i): singleton version;
2009-03-29 wenzelm 2009-03-29 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML; tuned;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-19 wenzelm 2009-03-19 use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-11 wenzelm 2009-03-11 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 wenzelm 2009-03-11 Thm.def_binding_optional;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 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; minor tuning;
2009-03-03 wenzelm 2009-03-03 Binding.str_of; pretty_name_atts: check Binding.is_empty, not result of Binding.str_of;
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-01-21 wenzelm 2009-01-21 eliminated obsolete var morphism; simplified map_ctxt: just one version, without var; removed obsolete params_of, prems_of, facts_of; removed obsolete rename operations; tuned;
2009-01-21 haftmann 2009-01-21 refined witness algebra
2009-01-17 haftmann 2009-01-17 explicit equation morphism
2008-12-16 ballarin 2008-12-16 Transfer morphism with theory closure.
2008-12-16 ballarin 2008-12-16 Finer-grained activation so that facts from earlier elements are available.
2008-12-16 ballarin 2008-12-16 Use correct mode when parsing elements and conclusion.
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-25 ballarin 2008-11-25 Use standard export function.
2008-11-20 haftmann 2008-11-20 tuned name bindings
2008-11-19 ballarin 2008-11-19 Basic types not qualified.
2008-11-18 ballarin 2008-11-18 Activate elements moved to element.ML.
2008-11-13 haftmann 2008-11-13 diagnostic output for name bindings
2008-11-10 haftmann 2008-11-10 more verbose element printing
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements; name/var morphism operates on Name.binding;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-04-18 wenzelm 2008-04-18 tuned;
2008-04-17 wenzelm 2008-04-17 print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-12-21 ballarin 2007-12-21 Fixed eta constraction issue in compose_witness
2007-12-14 wenzelm 2007-12-14 added close_witness;
2007-11-05 wenzelm 2007-11-05 tuned satisfy_thm;
2007-11-05 ballarin 2007-11-05 Removed inst_morphism'; satisfy_thm avoids compose.
2007-10-26 wenzelm 2007-10-26 proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;