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
2009-01-17 ago explicit equation morphism
2008-12-16 ago Transfer morphism with theory closure.
2008-12-16 ago Finer-grained activation so that facts from earlier elements are available.
2008-12-16 ago Use correct mode when parsing elements and conclusion.
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-11-25 ago Use standard export function.
2008-11-20 ago tuned name bindings
2008-11-19 ago Basic types not qualified.
2008-11-18 ago Activate elements moved to element.ML.
2008-11-13 ago diagnostic output for name bindings
2008-11-10 ago more verbose element printing
2008-09-02 ago type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-04-18 ago tuned;
2008-04-17 ago print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
2008-04-12 ago replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2007-12-21 ago Fixed eta constraction issue in compose_witness
2007-12-14 ago added close_witness;
2007-11-05 ago tuned satisfy_thm;
2007-11-05 ago Removed inst_morphism'; satisfy_thm avoids compose.
2007-10-26 ago proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-09-18 ago New function inst_morphism'.
2007-08-03 ago replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-06-18 ago tuned conjunction tactics: slightly smaller proof terms;
2007-06-13 ago Method.Basic: include position;
2007-05-10 ago moved conversions to structure Conv;
2007-04-15 ago Thm.fold_terms;
2007-04-14 ago inst(T)_morphism: avoid reference to static theory value;
2007-04-13 ago Experimental interpretation code for definitions.