| Wed, 07 Apr 2010 11:05:11 +0200 | Christian Urban | simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle | file | diff | annotate |
| Tue, 23 Mar 2010 12:20:27 -0700 | huffman | sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod | file | diff | annotate |
| Thu, 18 Mar 2010 13:59:20 +0100 | blanchet | merged | file | diff | annotate |
| Thu, 18 Mar 2010 12:58:52 +0100 | blanchet | now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp" | file | diff | annotate |
| Thu, 18 Mar 2010 13:56:31 +0100 | haftmann | generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add | file | diff | annotate |
| Thu, 11 Mar 2010 14:38:13 +0100 | haftmann | moved cardinality to Finite_Set as far as appropriate; added locales for fold_image | file | diff | annotate |
| Wed, 10 Mar 2010 16:53:27 +0100 | haftmann | split off theory Big_Operators from theory Finite_Set | file | diff | annotate | base |