| 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
|
| Tue, 08 Mar 2016 21:07:46 +0100 |
haftmann |
syntax for multiset membership modelled after syntax for set membership
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 22:44:11 +0100 |
haftmann |
more succint formulation of membership for multisets, similar to lists;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Fri, 19 Feb 2016 13:40:50 +0100 |
hoelzl |
generalize more theorems to support enat and ennreal
|
file |
diff |
annotate
|
| Wed, 10 Feb 2016 18:43:19 +0100 |
hoelzl |
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
|
file |
diff |
annotate
|
| Thu, 18 Feb 2016 17:53:09 +0100 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Wed, 20 Jan 2016 17:14:53 +0100 |
blanchet |
added 'supset' variants for new '<#' etc. symbols on multisets
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 13:04:31 +0100 |
blanchet |
nicer 'Spec_Rules' for size function
|
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
|
| Sat, 19 Dec 2015 11:05:04 +0100 |
haftmann |
abandoned attempt to unify sublocale and interpretation into global theories
|
file |
diff |
annotate
|
| Sat, 12 Dec 2015 16:32:00 +0100 |
haftmann |
modernized
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 17:44:32 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 15:14:28 +0200 |
wenzelm |
fewer aliases for toplevel theorem statements;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 11:50:23 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Thu, 17 Sep 2015 15:47:24 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 13:07:45 +0200 |
haftmann |
more lemmas on sorting and multisets (due to Thomas Sewell)
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 22:44:02 +0200 |
haftmann |
formal class for factorial (semi)rings
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:06:02 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 30 Jun 2015 13:29:30 +0200 |
hoelzl |
fix tex-output for rel_mset
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 16:07:55 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 15:41:16 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 15:36:29 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 15:55:22 +0200 |
nipkow |
renamed multiset_of -> mset
|
file |
diff |
annotate
|
| Thu, 18 Jun 2015 16:16:17 +0200 |
nipkow |
multiset_of_set -> mset_set
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 18:22:29 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 17:54:09 +0200 |
wenzelm |
manual merge;
|
file |
diff |
annotate
|