src/Pure/Isar/attrib.ML
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-01-26 wenzelm 2008-01-26 misc tuning and internal rearrangement; tuned attribute syntax -- no need for eta-expansion;
2007-09-26 wenzelm 2007-09-26 added eval_thms;
2007-09-25 wenzelm 2007-09-25 tuned functor application;
2007-08-13 kleing 2007-08-13 new attribute [rotated]
2007-08-07 wenzelm 2007-08-07 turned Unify flags into configuration options (global only);
2007-08-02 wenzelm 2007-08-02 turned simp_depth_limit into configuration option; tuned register_config;
2007-08-01 wenzelm 2007-08-01 tuned config options: eliminated separate attribute "option";
2007-07-28 wenzelm 2007-07-28 attribute "option": proper naming within the theory
2007-07-28 wenzelm 2007-07-28 tuned;
2007-07-27 wenzelm 2007-07-27 renamed Config to ConfigOption; thm scanners: added [[declaration]] syntax (abbreviates dummy_thm [att]);
2007-07-27 wenzelm 2007-07-27 attribute "option": more elaborate syntax (with value parsing);
2007-07-25 wenzelm 2007-07-25 added attribute "option" for setting configuration options;
2007-07-23 wenzelm 2007-07-23 eliminated transform_failure (to avoid critical section for main transactions);
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality;
2007-05-24 haftmann 2007-05-24 tuned Pure/General/name_space.ML
2007-05-10 wenzelm 2007-05-10 moved conversions to structure Conv;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-14 wenzelm 2007-04-14 Morphism.transform/form;
2007-04-03 wenzelm 2007-04-03 renamed Variable.import to import_thms (avoid clash with Alice keywords);
2007-01-19 wenzelm 2007-01-19 removed obsolete Attribute;
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-12-07 wenzelm 2006-12-07 thms etc.: proper treatment of internal_fact with selection;
2006-12-05 wenzelm 2006-12-05 Attrib.internal: morphism;
2006-11-21 wenzelm 2006-11-21 removed kind attribs;
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;