| 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
|
| Sun, 18 Sep 2016 11:31:19 +0200 |
fleury |
support replicate_mset in multiset simproc
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 11:48:20 +0200 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
| Tue, 13 Sep 2016 07:59:20 +0200 |
nipkow |
more lemmas
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 08:23:59 +0200 |
fleury |
delete looping simp rule
|
file |
diff |
annotate
|
| Sat, 10 Sep 2016 14:11:04 +0200 |
nipkow |
more simp
|
file |
diff |
annotate
|
| Fri, 09 Sep 2016 15:12:40 +0200 |
nipkow |
msetsum -> set_mset, msetprod -> prod_mset
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 15:47:50 +0200 |
fleury |
tuning multisets; more interpretations
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 15:47:50 +0200 |
fleury |
clean argument of simp add
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 15:47:50 +0200 |
fleury |
add_mset constructor in multisets
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
tuning whitespace in output syntax
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 14:01:49 +0200 |
Bertram Felgenhauer |
add monotonicity propertyies of `mult1` and `mult`
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 08:22:59 +0200 |
fleury |
more instantiations for multiset
|
file |
diff |
annotate
|
| Mon, 25 Jul 2016 11:30:31 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 08:02:37 +0200 |
wenzelm |
tuned proofs -- avoid improper use of "this";
|
file |
diff |
annotate
|
| Thu, 21 Jul 2016 10:06:04 +0200 |
eberlm |
Overhaul of prime/multiplicity/prime_factors
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 13:51:38 +0200 |
fleury |
adding mset_map to the simp rules
|
file |
diff |
annotate
|
| Thu, 07 Jul 2016 17:34:39 +0200 |
fleury |
more instantiations for multiset
|
file |
diff |
annotate
|
| Thu, 07 Jul 2016 09:24:03 +0200 |
blanchet |
moved lemmas and locales around (with minor incompatibilities)
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 13:05:04 +0200 |
fleury |
instantiate multiset with multiset ordering
|
file |
diff |
annotate
|
| Fri, 01 Jul 2016 10:56:54 +0200 |
Manuel Eberl |
Tuned multiset lattice
|
file |
diff |
annotate
|
| Fri, 01 Jul 2016 08:19:53 +0200 |
Manuel Eberl |
Conditionally complete lattice of multisets
|
file |
diff |
annotate
|
| Fri, 17 Jun 2016 12:37:43 +0200 |
fleury |
normalising multiset theorem names
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:22:42 +0200 |
haftmann |
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
|
file |
diff |
annotate
|
| Wed, 01 Jun 2016 13:48:34 +0200 |
eberlm |
Tuned code equations for mappings and PMFs
|
file |
diff |
annotate
|
| Tue, 17 May 2016 17:05:35 +0200 |
eberlm |
Moved material from AFP/Randomised_Social_Choice to distribution
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Thu, 12 May 2016 14:38:53 +0200 |
haftmann |
clarified heading
|
file |
diff |
annotate
|
| Thu, 12 May 2016 09:34:07 +0200 |
haftmann |
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 22:44:31 +0200 |
wenzelm |
some uses of 'obtain' with structure statement;
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Sun, 03 Apr 2016 23:03:30 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 12:48:00 +0100 |
nipkow |
superfluous premise (noticed by Julian Nagele)
|
file |
diff |
annotate
|