| Sat, 25 Jun 2022 13:21:27 +0200 |
desharna |
moved mono and strict_mono to Fun and redefined them as abbreviations
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Mon, 27 Jun 2022 15:54:18 +0200 |
traytel |
strict bounds for BNFs (by Jan van Brügge)
|
file |
diff |
annotate
|
| Fri, 24 Jun 2022 10:49:40 +0200 |
desharna |
added lemma monotone_on_o
|
file |
diff |
annotate
|
| Fri, 24 Jun 2022 15:05:04 +0200 |
desharna |
redefined mono_on and strict_mono_on as an abbreviation of monotone_on
|
file |
diff |
annotate
|
| Thu, 23 Jun 2022 19:29:22 +0200 |
desharna |
changed argument order of mono_on and strict_mono_on to uniformize with monotone_on and other predicates
|
file |
diff |
annotate
|
| Tue, 21 Jun 2022 13:40:35 +0200 |
desharna |
added lemmas monotone_on_empty[simp] and monotone_on_subset
|
file |
diff |
annotate
|
| Tue, 21 Jun 2022 13:39:06 +0200 |
desharna |
added predicate monotone_on and redefined monotone to be an abbreviation.
|
file |
diff |
annotate
|
| Thu, 05 Aug 2021 07:12:49 +0000 |
haftmann |
clarified abstract and concrete boolean algebras
|
file |
diff |
annotate
|
| Mon, 02 Aug 2021 10:01:06 +0000 |
haftmann |
moved theory Bit_Operations into Main corpus
|
file |
diff |
annotate
|
| Wed, 05 May 2021 16:09:02 +0000 |
haftmann |
tuned theory structure
|
file |
diff |
annotate
|
| Fri, 23 Apr 2021 09:50:14 +0000 |
haftmann |
collecting more lemmas concerning multisets
|
file |
diff |
annotate
|
| Mon, 22 Mar 2021 10:49:51 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sun, 28 Feb 2021 20:13:07 +0000 |
haftmann |
lemma diffusion
|
file |
diff |
annotate
|
| Sun, 28 Feb 2021 20:13:07 +0000 |
haftmann |
dissolve theory with duplicated name from afp
|
file |
diff |
annotate
|
| Sun, 09 Aug 2020 13:18:40 +0100 |
paulson |
elimination of some needless assumptions
|
file |
diff |
annotate
|
| Sat, 23 May 2020 21:24:33 +0100 |
paulson |
a few new lemmas about functions
|
file |
diff |
annotate
|
| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| Sun, 29 Mar 2020 15:44:54 +0100 |
paulson |
more tidying up of old apply-proofs
|
file |
diff |
annotate
|
| Wed, 26 Feb 2020 12:21:48 +0000 |
paulson |
Moved a number of general-purpose lemmas into HOL
|
file |
diff |
annotate
|
| Mon, 24 Feb 2020 12:14:13 +0000 |
paulson |
a few new lemmas
|
file |
diff |
annotate
|
| Mon, 27 Jan 2020 14:32:43 +0000 |
paulson |
A few lemmas connected with orderings
|
file |
diff |
annotate
|
| Thu, 14 Mar 2019 16:55:06 +0100 |
wenzelm |
more specific keyword kinds;
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Thu, 24 Jan 2019 14:44:52 +0000 |
paulson |
the theory of Equipollence, and moving Fpow from Cardinals into Main
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 14:44:23 +0000 |
paulson |
new material about summations and powers, along with some tweaks
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 23 Dec 2018 20:51:23 +0000 |
haftmann |
more rules
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Tue, 19 Dec 2017 13:58:12 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 13:47:35 +0100 |
haftmann |
restored surj as output abbreviation, amending 6af79184bef3
|
file |
diff |
annotate
|
| Sun, 29 Jan 2017 17:27:02 +0100 |
wenzelm |
added inj_def (redundant, analogous to surj_def, bij_def);
|
file |
diff |
annotate
|
| Sun, 29 Jan 2017 13:58:03 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 22:36:53 +0200 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 21:05:34 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 01 Aug 2016 22:11:29 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 09:49:23 +0200 |
Andreas Lochbihler |
add lemmas contributed by Peter Gammie
|
file |
diff |
annotate
|
| Fri, 08 Jul 2016 23:43:11 +0200 |
haftmann |
avoid to hide equality behind (output) abbreviation
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 23:39:49 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Mon, 20 Jun 2016 17:51:47 +0200 |
wenzelm |
prefer HOL definitions;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2016 17:25:08 +0200 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2016 17:03:50 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 09 May 2016 16:02:23 +0100 |
paulson |
renamings and refinements
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 16:52:56 +0100 |
paulson |
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
|
file |
diff |
annotate
|
| Mon, 14 Mar 2016 14:19:06 +0000 |
paulson |
Refactoring (moving theorems into better locations), plus a bit of new material
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 18 Nov 2015 15:23:34 +0000 |
paulson |
New theorems mostly from Peter Gammie
|
file |
diff |
annotate
|
| Wed, 11 Nov 2015 09:48:24 +0100 |
Andreas Lochbihler |
add various lemmas
|
file |
diff |
annotate
|
| Tue, 27 Oct 2015 15:17:02 +0000 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 19:52:13 +0100 |
paulson |
new lemmas and movement of lemmas into place
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 10:05:58 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 26 May 2015 21:58:04 +0100 |
paulson |
New material about paths, and some lemmas
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 13:47:48 +0100 |
Andreas Lochbihler |
add lemmas about bind and image
|
file |
diff |
annotate
|