src/Pure/Isar/attrib.ML
2005-11-23 wenzelm 2005-11-23 added case_conclusion attribute;
2005-10-28 wenzelm 2005-10-28 syntax for literal facts;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-29 wenzelm 2005-08-29 use AList operations;
2005-08-18 wenzelm 2005-08-18 added map_specs/facts operators (from locale.ML);
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify;
2005-06-20 wenzelm 2005-06-20 thmref: Name vs. NameSelection;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-06-09 wenzelm 2005-06-09 attribs: NameSpace.table;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern; Sign.declare_name replaces NameSpace.extend;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-05-04 berghofe 2005-05-04 Added eta_long attribute.
2005-04-23 wenzelm 2005-04-23 qualified name Pure.attribute;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** type src = Args.src; renamed local_attribute' to context_attribute; added _i versions of global/local/context_attribute and separate intern/intern_src; added crude_closure to produce argument closure without knowing facts in advance; added 'attribute' to embed internal attributes into src; removed multi_attribute etc.; moved thm_sel to args.ML; Scan.peek; read_instantiate/'where'/'of': support arbitrary mix of external / internal typ / term args, with proper treatment of static binding;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Specific theorems in a named list of theorems can now be referred to via indices (type thmref).
2004-08-06 paulson 2004-08-06 RS -> THEN
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-07 wenzelm 2004-05-07 tuned;
2003-12-10 ballarin 2003-12-10 Isar: where attribute supports instantiation of type variables.
2003-11-14 ballarin 2003-11-14 Type inference bug in Isar attributes "where" and "of" fixed.
2003-06-29 berghofe 2003-06-29 Moved function for renaming bound variables to Pure/drule.ML
2003-01-17 berghofe 2003-01-17 Added rename_abs attribute for renaming bound variables.
2002-07-24 wenzelm 2002-07-24 removed attribute "norm_hhf";
2002-07-16 wenzelm 2002-07-16 context rules;
2002-01-17 wenzelm 2002-01-17 Tactic.norm_hhf renamed to Tactic.norm_hhf_rule;
2002-01-16 wenzelm 2002-01-16 norm_hhf;
2001-12-05 wenzelm 2001-12-05 removed bang_args;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
2001-10-23 wenzelm 2001-10-23 removed obsolete "exported" att;
2001-10-15 wenzelm 2001-10-15 bang_args;
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-14 wenzelm 2001-10-14 added 'atomize' attribute;
2001-10-12 wenzelm 2001-10-12 removed read_inst', no longer export insts';
2001-01-06 wenzelm 2001-01-06 export read_inst', inst'; tuned;
2000-11-28 wenzelm 2000-11-28 added "consumes" attribute;
2000-10-04 wenzelm 2000-10-04 'THEN', 'COMP': improved optional position arg;
2000-09-19 wenzelm 2000-09-19 tuned args;
2000-09-13 wenzelm 2000-09-13 Args.addN, Args.delN;
2000-09-12 wenzelm 2000-09-12 renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-07 wenzelm 2000-09-07 improved att names / msgs;
2000-08-17 wenzelm 2000-08-17 renamed 'RS' to 'THEN';
2000-07-01 wenzelm 2000-07-01 removed help_attributes;
2000-05-31 wenzelm 2000-05-31 removed 'transfer' att (is now automatic);
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-17 wenzelm 2000-04-17 Pretty.chunks;
2000-04-12 wenzelm 2000-04-12 Args.name_dummy;
2000-03-31 wenzelm 2000-03-31 added add_del_args;
2000-03-17 wenzelm 2000-03-17 untag: remove all tags of given name;
2000-03-08 wenzelm 2000-03-08 added 'case_names' and 'params';
2000-02-22 wenzelm 2000-02-22 tuned syntax wrapper;