| Tue, 05 Jan 2021 03:35:46 +0100 |
Manuel Eberl |
HOL-Library.Multiset: new notation for prod_mset, consistent with sum_mset
|
file |
diff |
annotate
|
| Mon, 04 Jan 2021 19:41:38 +0100 |
Manuel Eberl |
HOL-Library: Changed notation for sum_mset
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 07:17:06 +0000 |
haftmann |
bundles for reflected term syntax
|
file |
diff |
annotate
|
| Thu, 12 Nov 2020 09:06:44 +0100 |
haftmann |
bundled syntax for state monad combinators
|
file |
diff |
annotate
|
| Wed, 03 Jun 2020 11:44:21 +0200 |
nipkow |
should have been copied across from Set.thy as well for better printing
|
file |
diff |
annotate
|
| Tue, 21 Jan 2020 11:02:27 +0100 |
Manuel Eberl |
Removed multiplicativity assumption from normalization_semidom
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 23:23:03 +0100 |
wenzelm |
more formal contributors (with the help of the history);
|
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
|
| Mon, 10 Dec 2018 20:35:08 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 09:11:52 +0100 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
file |
diff |
annotate
|
| Wed, 03 Oct 2018 09:46:42 +0200 |
nipkow |
shuffle -> shuffles
|
file |
diff |
annotate
|
| Sun, 23 Sep 2018 12:50:12 +0200 |
nipkow |
use standard syntax
|
file |
diff |
annotate
|
| Fri, 14 Sep 2018 07:31:55 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 13 Sep 2018 16:15:05 +0200 |
nipkow |
removed redundant lemma
|
file |
diff |
annotate
|
| Thu, 13 Sep 2018 13:09:03 +0200 |
nipkow |
more simp lemmas
|
file |
diff |
annotate
|
| Thu, 13 Sep 2018 08:36:51 +0200 |
nipkow |
prefer explicit
|
file |
diff |
annotate
|
| Thu, 13 Sep 2018 06:36:00 +0200 |
nipkow |
typo
|
file |
diff |
annotate
|
| Wed, 12 Sep 2018 18:44:31 +0200 |
nipkow |
added spaces because otherwise nonatomic arguments look awful: BIGf x -> BIG f x
|
file |
diff |
annotate
|
| Sat, 08 Sep 2018 08:08:28 +0000 |
haftmann |
left-over rename from 3f9bb52082c4
|
file |
diff |
annotate
|
| Thu, 07 Jun 2018 19:36:12 +0200 |
nipkow |
utilize 'flip'
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 11:12:37 +0200 |
nipkow |
Keep filter input syntax
|
file |
diff |
annotate
|
| Tue, 22 May 2018 11:08:37 +0200 |
nipkow |
First step to remove nonstandard "[x <- xs. P]" syntax: only input
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 13:56:16 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:21:49 +0100 |
nipkow |
Manual updates towards conversion of "op" syntax
|
file |
diff |
annotate
|
| Wed, 03 Jan 2018 11:06:13 +0100 |
blanchet |
kill old size infrastructure
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 13:18:44 +0000 |
haftmann |
generalized some lemmas on multisets
|
file |
diff |
annotate
|
| Thu, 24 Aug 2017 10:47:56 +0200 |
blanchet |
tuning (proofs and code)
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 19:47:08 +0200 |
nipkow |
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 09:29:35 +0200 |
nipkow |
added Min_mset and Max_mset
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 23:03:44 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Sat, 15 Jul 2017 14:32:02 +0100 |
eberlm |
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 21:37:01 +0200 |
blanchet |
moved lemmas from AFP to Isabelle
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 21:06:02 +0200 |
blanchet |
two new induction principles on multisets
|
file |
diff |
annotate
|
| Wed, 12 Apr 2017 09:27:47 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 03 Apr 2017 22:18:56 +0200 |
eberlm |
removed problematic simp rule
|
file |
diff |
annotate
|
| Mon, 03 Apr 2017 16:56:45 +0200 |
eberlm |
added shuffle product to HOL/List
|
file |
diff |
annotate
|
| Fri, 24 Feb 2017 13:59:50 +0100 |
blanchet |
added multiset lemma
|
file |
diff |
annotate
|
| Fri, 24 Feb 2017 13:59:49 +0100 |
blanchet |
added multiset lemma
|
file |
diff |
annotate
|
| Thu, 16 Feb 2017 13:54:22 +0100 |
fleury |
use the cancellation simprocs directly
|
file |
diff |
annotate
|
| Tue, 14 Feb 2017 18:32:53 +0100 |
fleury |
cancellation simprocs generalising the multiset simprocs
|
file |
diff |
annotate
|
| Mon, 13 Feb 2017 16:03:53 +0100 |
fleury |
renaming multiset simprocs
|
file |
diff |
annotate
|
| Tue, 17 Jan 2017 13:59:10 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
restructured matter on polynomials and normalized fractions
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
standardized notation
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:00 +0100 |
haftmann |
redundant
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:00 +0100 |
haftmann |
renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
|
file |
diff |
annotate
|
| Tue, 29 Nov 2016 08:32:44 +0100 |
blanchet |
added lemma about 'mult', as suggested by Bertram Felgenhauer
|
file |
diff |
annotate
|
| Thu, 27 Oct 2016 15:51:54 +0200 |
fleury |
more lemmas
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Fri, 07 Oct 2016 17:59:19 +0200 |
fleury |
more lemmas
|
file |
diff |
annotate
|
| Fri, 07 Oct 2016 17:58:36 +0200 |
fleury |
tuning multisets
|
file |
diff |
annotate
|
| Fri, 07 Oct 2016 17:57:17 +0200 |
fleury |
more lemmas
|
file |
diff |
annotate
|
| Wed, 05 Oct 2016 20:12:56 +0200 |
fleury |
more multiset simp rules
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 17:57:55 +0200 |
haftmann |
more generic algebraic lemmas
|
file |
diff |
annotate
|
| Tue, 20 Sep 2016 11:35:10 +0200 |
eberlm |
Merged
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 17:37:22 +0200 |
eberlm |
Additions to permutations (contributed by Lukas Bulwahn)
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:07:39 +0200 |
fleury |
# after multiset intersection and union symbol
|
file |
diff |
annotate
|