src/HOL/Tools/split_rule.ML
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2010-11-06 krauss 2010-11-06 abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-05-28 haftmann 2010-05-28 avoid reference to thm PairE
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-04-30 wenzelm 2010-04-30 proper context for rule_by_tactic;
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