src/Pure/Isar/attrib.ML
2006-10-14 wenzelm 2006-10-14 added pretty_attribs (from attrib.ML);
2006-10-09 wenzelm 2006-10-09 added kind attributes;
2006-08-03 wenzelm 2006-08-03 moved read_instantiate etc. to rule_insts.ML;
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-07-27 wenzelm 2006-07-27 no_vars: based on Variable.import; tuned;
2006-07-06 wenzelm 2006-07-06 thm parsers: include Args.internal_fact;
2006-06-06 wenzelm 2006-06-06 tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-10 wenzelm 2006-02-10 Context.generic is canonical state of parsers; removed obsolete global/local parsers; tuned interfaces;
2006-02-08 haftmann 2006-02-08 introduced gen_distinct in place of distinct
2006-02-02 wenzelm 2006-02-02 more generic type for map_specs/facts;
2006-01-31 wenzelm 2006-01-31 (un)folded: removed '(raw)' option;
2006-01-29 wenzelm 2006-01-29 added 'defn' attribute; attribute (un)folded: option '(raw)';
2006-01-28 wenzelm 2006-01-28 (un)folded: support object-level rewrites;
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy;
2006-01-21 wenzelm 2006-01-21 simplified type attribute; removed rule/declaration (cf. thm.ML); removed obsolete theory/proof/generic/common; removed obsolete global/local/context_attribute(_i); added attribute(_i); renamed attribute to internal;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-10 wenzelm 2006-01-10 added rule, declaration; support generic attributes: theory, context, generic, common, generic_attribute(_i); added generic syntax; basic attributes now generic; tuned;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-11-24 wenzelm 2005-11-24 fixed spelling of 'case_conclusion';
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;