src/HOL/Tools/split_rule.ML
2010-02-25 wenzelm 2010-02-25 modernized structure Split_Rule; tuned signature; more antiquotations;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-07-30 haftmann 2009-07-30 path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
2009-07-29 haftmann 2009-07-29 cleaned up abstract tuple operations and named them consistently
2009-07-29 haftmann 2009-07-29 cleaned up abstract tuple operations and named them consistently
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-08-15 wenzelm 2008-08-15 Args.name_source(_position) for proper position information;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-14 wenzelm 2008-06-14 proper context for tactics derived from res_inst_tac;
2008-03-20 haftmann 2008-03-20 tuned
2008-01-26 wenzelm 2008-01-26 tuned attribute syntax -- no need for eta-expansion;
2007-09-15 haftmann 2007-09-15 fixed title
2007-02-07 berghofe 2007-02-07 Added split_rule attribute.
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-05-27 wenzelm 2006-05-27 complete_split_rule: all Vars; tuned;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-10 wenzelm 2006-01-10 Attrib.rule;
2005-10-31 haftmann 2005-10-31 fold_index replacing foldln
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-10-19 wenzelm 2001-10-19 got rid of ML proof scripts for Product_Type;
2001-02-03 wenzelm 2001-02-03 fixed syntax of 'split_format';
2001-02-03 wenzelm 2001-02-03 simplified 'split_format' syntax;
2001-02-02 wenzelm 2001-02-02 module setup; use hidden internal_split constants;
2001-02-01 oheimb 2001-02-01 converted to Isar therory, adding attributes complete_split and split_format