| Wed, 01 Feb 2023 20:21:33 +0100 |
wenzelm |
isabelle update -u cite -l "";
|
file |
diff |
annotate
|
| Mon, 15 Aug 2022 12:50:24 +0100 |
paulson |
The same, without adding a new simprule
|
file |
diff |
annotate
|
| Sun, 14 Aug 2022 23:51:47 +0100 |
paulson |
moved some material from Sum_of_Powers
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 20:08:24 +0100 |
paulson |
The right way to formulate card_UNION, plus the old version for compatibility
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Fri, 25 Sep 2020 14:11:48 +0100 |
paulson |
fixed some remarkably ugly proofs
|
file |
diff |
annotate
|
| Mon, 06 Apr 2020 22:46:55 +0100 |
paulson |
removed more applys
|
file |
diff |
annotate
|
| Mon, 06 Apr 2020 19:46:38 +0100 |
paulson |
a few more applys
|
file |
diff |
annotate
|
| Tue, 07 Jan 2020 07:03:18 +0100 |
nipkow |
generalized thm (as suggested by Christian Weinz)
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 21:29:32 +0100 |
paulson |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 13:34:55 +0100 |
paulson |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2018 09:46:42 +0200 |
nipkow |
shuffle -> shuffles
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 12:32:58 +0000 |
haftmann |
more uniform parameter naming convention for choose and gchoose
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 12:32:58 +0000 |
haftmann |
slightly generalized theorems
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 12:32:58 +0000 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 12:32:58 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 03 May 2018 22:34:49 +0100 |
paulson |
Some tidying up (mostly regarding summations from 0)
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Sat, 13 Jan 2018 09:18:54 +0000 |
haftmann |
restored naming of lemmas after corresponding constants
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Fri, 29 Dec 2017 19:17:52 +0100 |
wenzelm |
prefer formal citations;
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 09:30:09 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Fri, 12 May 2017 20:03:50 +0200 |
haftmann |
relaxed theory dependencies
|
file |
diff |
annotate
|
| Fri, 12 May 2017 07:53:35 +0200 |
haftmann |
explicit theory for factorials
|
file |
diff |
annotate
|
| Wed, 26 Apr 2017 13:41:32 +0200 |
eberlm |
better code equation for binomial
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|