| 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
|
| Fri, 05 Apr 2019 15:02:46 +0100 |
paulson |
Free_Abelian_Groups finally working; fixed some duplicates; cleaned up some proofs
|
file |
diff |
annotate
|
| Thu, 04 Apr 2019 14:19:33 +0100 |
paulson |
More group theory. Sum and product indexed by the non-neutral part of a set
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Mon, 28 Jan 2019 18:36:50 -0500 |
immler |
less odd class.second_countable_topology_def
|
file |
diff |
annotate
|
| Mon, 28 Jan 2019 10:27:47 +0100 |
nipkow |
more canonical and less specialized syntax
|
file |
diff |
annotate
|
| Fri, 25 Jan 2019 13:19:16 +0100 |
nipkow |
moved retracts
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:38:00 -0500 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 19:34:48 -0500 |
immler |
chapters for analysis manual
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 12:31:08 +0100 |
immler |
moved material from Connected.thy to more appropriate places
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 11:29:34 +0100 |
immler |
moved material from Connected.thy to more appropriate places
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 17:54:49 +0100 |
immler |
moved some material from Connected.thy to more appropriate places
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 13:26:37 +0100 |
nipkow |
tuned defs
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 20:32:09 +0100 |
immler |
split off theorems involving classes below metric_space and real_normed_vector
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 15:43:53 +0100 |
nipkow |
capitalize proper names in lemma names
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 23:38:55 +0100 |
immler |
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
|
file |
diff |
annotate
|