| 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 |
| 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 |