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