Wed, 02 Dec 2015 19:14:56 +0100 |
haftmann |
formally correct context for export, which got screwed up in 87203a0f0041
|
changeset |
files
|
Wed, 02 Dec 2015 19:14:55 +0100 |
haftmann |
tuned whitespace
|
changeset |
files
|
Tue, 01 Dec 2015 22:24:37 +0100 |
blanchet |
removed needless ML function
|
changeset |
files
|
Tue, 01 Dec 2015 22:21:40 +0100 |
blanchet |
tuned whitespace
|
changeset |
files
|
Tue, 01 Dec 2015 22:21:37 +0100 |
blanchet |
reverted inadvertently qfinished/pushed change r164eeb2ab675
|
changeset |
files
|
Tue, 01 Dec 2015 17:18:34 +0100 |
Andreas Lochbihler |
merged
|
changeset |
files
|
Tue, 01 Dec 2015 12:35:11 +0100 |
Andreas Lochbihler |
add formalisation of Bourbaki-Witt fixpoint theorem
|
changeset |
files
|
Tue, 01 Dec 2015 12:28:02 +0100 |
Andreas Lochbihler |
add lemmas
|
changeset |
files
|
Tue, 01 Dec 2015 12:27:16 +0100 |
Andreas Lochbihler |
strengthen lemma
|
changeset |
files
|
Tue, 01 Dec 2015 14:19:25 +0000 |
paulson |
Merge
|
changeset |
files
|
Tue, 01 Dec 2015 14:09:10 +0000 |
paulson |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
changeset |
files
|
Tue, 01 Dec 2015 13:07:41 +0100 |
blanchet |
set "transfer_rule" attribute more generously
|
changeset |
files
|