src/Pure/Isar/attrib.ML
2009-03-18 wenzelm 2009-03-18 more precise type Symbol_Pos.text;
2009-03-16 wenzelm 2009-03-16 tuned signature;
2009-03-15 wenzelm 2009-03-15 added setup and attribute_setup -- expect plain parser instead of syntax function; aded add_del parser;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-12 wenzelm 2009-03-12 renamed NameSpace.bind to NameSpace.define;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-29 berghofe 2009-01-29 Added abs_def attribute.
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
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-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-10 wenzelm 2008-08-10 pass position to get_fact; tuned;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations; unified version of thm_sel (formerly in args.ML and spec_parse.ML);
2008-08-06 wenzelm 2008-08-06 report markup;
2008-08-04 wenzelm 2008-08-04 tuned signature; eliminated obsolete pervasives;
2008-05-14 wenzelm 2008-05-14 added defined;
2008-04-17 wenzelm 2008-04-17 no_vars: reset body mode, i.e. invent global frees (which are acceptable to Variable.auto_fixes);
2008-04-16 wenzelm 2008-04-16 PureThy.get_fact: pass dynamic context;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-20 wenzelm 2008-03-20 Facts.Named: include position;
2008-03-20 wenzelm 2008-03-20 renamed former get_thms(_silent) to get_fact(_silent);
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;