src/HOL/Fun_Def.thy
Mon, 22 Jan 2018 16:08:50 +0100 Lars Hupel drop redundant fundef_cong rule
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Sat, 17 Dec 2016 15:22:13 +0100 haftmann restructured matter on polynomials and normalized fractions
Wed, 10 Aug 2016 22:05:36 +0200 wenzelm misc tuning and modernization;
Mon, 11 Jul 2016 09:57:20 +0200 wenzelm tuned;
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Thu, 27 Aug 2015 21:19:48 +0200 haftmann standardized some occurences of ancient "split" alias
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 07 Jul 2015 18:37:24 +0200 blanchet have the installed termination prover take a 'quiet' flag
Wed, 08 Apr 2015 11:52:53 +0200 wenzelm tuned signature;
Mon, 15 Dec 2014 07:20:48 +0100 blanchet renamed theory file
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
Wed, 29 Oct 2014 14:14:36 +0100 wenzelm modernized setup;
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved old 'size' generator together with 'old_datatype'
Thu, 11 Sep 2014 18:54:36 +0200 blanchet renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
Tue, 19 Aug 2014 12:05:11 +0200 wenzelm simplified type Proof.method;
Sat, 16 Aug 2014 19:20:11 +0200 wenzelm updated to named_theorems;
Sun, 04 May 2014 18:14:58 +0200 blanchet renamed 'xxx_size' to 'size_xxx' for old datatype package
Wed, 23 Apr 2014 10:23:27 +0200 blanchet move size hooks together, with new one preceding old one and sharing same theory data
Sat, 22 Mar 2014 08:37:43 +0100 haftmann generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
Fri, 07 Mar 2014 14:21:15 +0100 blanchet tuning
Fri, 14 Feb 2014 07:53:46 +0100 blanchet merged 'Option.map' and 'Option.map_option'
Mon, 20 Jan 2014 21:32:41 +0100 blanchet moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
less more (0) tip