2010-05-12 ago updated/unified some legacy warnings;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
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-10 ago constdefs is legacy
2010-03-07 ago modernized structure Local_Defs;
2009-11-19 ago replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
2009-11-05 ago declare Spec_Rules for most basic definitional packages;
2009-11-02 ago modernized structure Proof_Display;
2009-09-23 ago handling of definitions
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, 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-11 ago Thm.def_binding_optional;
2009-03-07 ago more uniform handling of binding in targets and derived elements;
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 Thm.binding;
2009-01-21 ago binding replaces bstring
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-09-26 ago removed obsolete name convention "func"
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-07-29 ago PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2007-11-08 ago discontinued legacy vars;
2007-11-07 ago discontinued ProofContext.read_prop_legacy;
2007-09-18 ago distinction between regular and default code theorems
2007-08-10 ago new structure for code generator modules
2007-04-26 ago renamed some old names to;
2007-04-20 ago defs are added to code data
2007-04-15 ago read prop as prop, not term;
2006-10-07 ago Thm.def_name_optional;
2006-02-06 ago LocalDefs.cert_def;
2006-01-31 ago tuned LocalTheory.pretty_consts;
2006-01-25 ago tuned comment;
2006-01-24 ago LocalTheory.pretty_consts;
2006-01-21 ago simplified type attribute;
2006-01-13 ago uniform handling of fixes;
2006-01-10 ago Specification.pretty_consts ctxt;
2006-01-07 ago Specification.pretty_consts;
2005-12-06 ago re-oriented some result tuples in PureThy
2005-10-15 ago tuned;
2005-08-16 ago replaced sign by thy;
2005-05-17 ago tuned;
2005-04-13 ago *** empty log message ***
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-29 ago license change to BSD
2004-05-07 ago be liberal about constant names;
2004-04-23 ago improved messages;
2004-04-22 ago 'constdefs' with automatic type-inference and structure context;