src/HOL/Tools/functor.ML
Sat, 30 Jul 2016 21:10:02 +0200 wenzelm tuned;
Mon, 23 May 2016 21:30:30 +0200 wenzelm embedded content may be delimited via cartouches;
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
Mon, 15 Jun 2015 16:24:52 +0200 wenzelm tuned signature;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Sun, 29 Mar 2015 18:18:52 +0200 wenzelm avoid low-level tsig operations;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Fri, 14 Feb 2014 07:53:46 +0100 blanchet renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
less more (0) tip