src/HOL/Fun.thy
Mon, 22 Mar 2021 10:49:51 +0000 haftmann more lemmas
Sun, 28 Feb 2021 20:13:07 +0000 haftmann lemma diffusion
Sun, 28 Feb 2021 20:13:07 +0000 haftmann dissolve theory with duplicated name from afp
Sun, 09 Aug 2020 13:18:40 +0100 paulson elimination of some needless assumptions
Sat, 23 May 2020 21:24:33 +0100 paulson a few new lemmas about functions
Mon, 11 May 2020 11:15:41 +0100 paulson the Uniq quantifier
Sun, 29 Mar 2020 15:44:54 +0100 paulson more tidying up of old apply-proofs
Wed, 26 Feb 2020 12:21:48 +0000 paulson Moved a number of general-purpose lemmas into HOL
Mon, 24 Feb 2020 12:14:13 +0000 paulson a few new lemmas
Mon, 27 Jan 2020 14:32:43 +0000 paulson A few lemmas connected with orderings
Thu, 14 Mar 2019 16:55:06 +0100 wenzelm more specific keyword kinds;
Thu, 31 Jan 2019 13:08:59 +0000 haftmann proper congruence rule for image operator
Thu, 24 Jan 2019 14:44:52 +0000 paulson the theory of Equipollence, and moving Fpow from Cardinals into Main
Mon, 21 Jan 2019 14:44:23 +0000 paulson new material about summations and powers, along with some tweaks
Mon, 14 Jan 2019 18:35:03 +0000 haftmann tuned proofs
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 23 Dec 2018 20:51:23 +0000 haftmann more rules
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Tue, 19 Dec 2017 13:58:12 +0100 wenzelm isabelle update_cartouches -c -t;
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
less more (0) -100 -60 tip