| Thu, 28 Jul 2022 12:33:20 +0100 |
paulson |
a few new theorems
|
file |
diff |
annotate
|
| Mon, 22 Mar 2021 10:49:51 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Fri, 25 Dec 2020 15:37:27 +0000 |
paulson |
A few more simprules for iff-reasoning
|
file |
diff |
annotate
|
| Fri, 25 Dec 2020 11:44:18 +0000 |
paulson |
infinite products iff simprule
|
file |
diff |
annotate
|
| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
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
|
| Tue, 01 Jan 2019 20:57:54 +0100 |
wenzelm |
retain important whitespace after 'text' that is suppressed, but swallows adjacent whitespace;
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 15:43:53 +0100 |
nipkow |
capitalize proper names in lemma names
|
file |
diff |
annotate
|
| Tue, 17 Jul 2018 12:23:37 +0200 |
Manuel Eberl |
tagged
|
file |
diff |
annotate
|
| Wed, 11 Jul 2018 23:24:25 +0100 |
paulson |
de-applying (mostly Quotient)
|
file |
diff |
annotate
|
| Wed, 04 Jul 2018 11:00:06 +0100 |
paulson |
infinite products: the final piece
|
file |
diff |
annotate
|
| Tue, 03 Jul 2018 14:46:14 +0100 |
paulson |
more on infinite products
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 20:48:49 +0100 |
paulson |
a few new lemmas
|
file |
diff |
annotate
|
| Fri, 15 Jun 2018 12:18:06 +0100 |
paulson |
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
|
file |
diff |
annotate
|
| Mon, 11 Jun 2018 16:23:21 +0100 |
paulson |
fixed a name clash
|
file |
diff |
annotate
|
| Mon, 11 Jun 2018 14:34:17 +0100 |
paulson |
the last of the infinite product proofs
|
file |
diff |
annotate
|
| Sun, 03 Jun 2018 15:22:30 +0100 |
paulson |
infinite product material
|
file |
diff |
annotate
|
| Thu, 10 May 2018 15:59:39 +0100 |
paulson |
auto-tidying
|
file |
diff |
annotate
|
| Thu, 10 May 2018 15:41:34 +0100 |
paulson |
more on infinite products
|
file |
diff |
annotate
|
| Wed, 09 May 2018 14:07:19 +0100 |
paulson |
more infinite product theorems
|
file |
diff |
annotate
|
| Thu, 03 May 2018 18:40:14 +0100 |
paulson |
tidied up Infinite_Products
|
file |
diff |
annotate
|
| Thu, 03 May 2018 17:14:08 +0100 |
paulson |
a lemma about infinite products
|
file |
diff |
annotate
|
| Wed, 02 May 2018 12:47:56 +0100 |
paulson |
type class generalisations; some work on infinite products
|
file |
diff |
annotate
|
| Sat, 15 Jul 2017 14:33:56 +0100 |
eberlm |
HOL-Analysis: Infinite products
|
file |
diff |
annotate
|