src/Pure/Isar/attrib.ML
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;
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)';