src/HOL/Tools/split_rule.ML
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Thu, 09 Jun 2011 23:12:02 +0200 wenzelm renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
Sat, 06 Nov 2010 00:10:32 +0100 krauss abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Fri, 28 May 2010 13:37:29 +0200 haftmann avoid reference to thm PairE
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Fri, 30 Apr 2010 18:06:29 +0200 wenzelm proper context for rule_by_tactic;
Thu, 25 Feb 2010 22:46:52 +0100 wenzelm modernized structure Split_Rule;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Thu, 30 Jul 2009 15:20:57 +0200 haftmann path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
Wed, 29 Jul 2009 16:54:20 +0200 haftmann cleaned up abstract tuple operations and named them consistently
Wed, 29 Jul 2009 16:48:34 +0200 haftmann cleaned up abstract tuple operations and named them consistently
less more (0) -15 tip