src/HOL/Fun.thy
Fri, 10 Mar 2017 13:47:35 +0100 haftmann restored surj as output abbreviation, amending 6af79184bef3
Sun, 29 Jan 2017 17:27:02 +0100 wenzelm added inj_def (redundant, analogous to surj_def, bij_def);
Sun, 29 Jan 2017 13:58:03 +0100 wenzelm tuned proofs;
Tue, 02 Aug 2016 22:36:53 +0200 wenzelm tuned proof;
Tue, 02 Aug 2016 21:05:34 +0200 wenzelm misc tuning and modernization;
Mon, 01 Aug 2016 22:11:29 +0200 wenzelm misc tuning and modernization;
Fri, 29 Jul 2016 09:49:23 +0200 Andreas Lochbihler add lemmas contributed by Peter Gammie
Fri, 08 Jul 2016 23:43:11 +0200 haftmann avoid to hide equality behind (output) abbreviation
Tue, 05 Jul 2016 23:39:49 +0200 wenzelm misc tuning and modernization;
Sat, 02 Jul 2016 08:41:05 +0200 haftmann more theorems
Mon, 20 Jun 2016 17:51:47 +0200 wenzelm prefer HOL definitions;
Mon, 20 Jun 2016 17:25:08 +0200 wenzelm tuned proof;
Mon, 20 Jun 2016 17:03:50 +0200 wenzelm misc tuning and modernization;
Mon, 09 May 2016 16:02:23 +0100 paulson renamings and refinements
Mon, 04 Apr 2016 16:52:56 +0100 paulson Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
Mon, 14 Mar 2016 14:19:06 +0000 paulson Refactoring (moving theorems into better locations), plus a bit of new material
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 18 Nov 2015 15:23:34 +0000 paulson New theorems mostly from Peter Gammie
Wed, 11 Nov 2015 09:48:24 +0100 Andreas Lochbihler add various lemmas
Tue, 27 Oct 2015 15:17:02 +0000 paulson Cauchy's integral formula, required lemmas, and a bit of reorganisation
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Mon, 21 Sep 2015 19:52:13 +0100 paulson new lemmas and movement of lemmas into place
Thu, 13 Aug 2015 10:05:58 +0200 haftmann more lemmas
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 26 May 2015 21:58:04 +0100 paulson New material about paths, and some lemmas
Wed, 11 Feb 2015 13:47:48 +0100 Andreas Lochbihler add lemmas about bind and image
Wed, 11 Feb 2015 12:01:56 +0000 paulson Merge
Tue, 10 Feb 2015 16:08:11 +0000 paulson New lemmas and a bit of tidying up.
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 30 Oct 2014 22:45:19 +0100 wenzelm eliminated aliases;
Sat, 06 Sep 2014 20:12:32 +0200 haftmann added various facts
Mon, 01 Sep 2014 16:17:46 +0200 blanchet tuned structure inclusion
Sat, 21 Jun 2014 10:41:02 +0200 ballarin Two basic lemmas on bij_betw.
Wed, 16 Apr 2014 21:51:41 +0200 haftmann more simp rules for Fun.swap
Sat, 15 Mar 2014 08:31:33 +0100 haftmann more complete set of lemmas wrt. image and composition
Thu, 13 Mar 2014 08:56:08 +0100 haftmann tuned proofs
Sun, 09 Mar 2014 22:45:09 +0100 haftmann bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices
Fri, 07 Mar 2014 22:30:58 +0100 wenzelm more antiquotations;
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)
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuning
Thu, 16 Jan 2014 16:50:41 +0100 blanchet moved lemmas from 'Fun_More_FP' to where they belong
Mon, 25 Nov 2013 10:14:29 +0100 traytel eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
Fri, 18 Oct 2013 10:43:20 +0200 blanchet killed most "no_atp", to make Sledgehammer more complete
Thu, 26 Sep 2013 15:50:33 +0200 Andreas Lochbihler add lemmas
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 03 Apr 2013 10:15:43 +0200 haftmann generalized lemma fold_image thanks to Peter Lammich
Thu, 18 Oct 2012 09:19:37 +0200 haftmann simp results for simplification results of Inf/Sup expressions on bool;
Mon, 08 Oct 2012 12:03:49 +0200 haftmann consolidated names of theorems on composition;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 19 Apr 2012 10:49:47 +0200 huffman tuned lemmas (v)image_id;
Sun, 15 Apr 2012 20:51:07 +0200 haftmann centralized enriched_type declaration, thanks to in-situ available Isar commands
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Wed, 22 Feb 2012 08:05:28 +0100 bulwahn generalizing inj_on_Int
Sun, 05 Feb 2012 08:47:13 +0100 bulwahn removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)
Sun, 05 Feb 2012 08:36:41 +0100 bulwahn adding a remark about lemma which is too special and should be removed
less more (0) -100 -60 tip