We have recently (e.g. #1398) added a number of very large and rather unwieldy proofs. While it is true that what matters is the spec, the proof files are so large that even finding the spec is not trivial -- in one instance, my browser could hardly handle it. So we should consider if we can clean up those proofs to make them more compact, and/or reorganize the proof files in general so that it is easier to find the specs.
We have recently (e.g. #1398) added a number of very large and rather unwieldy proofs. While it is true that what matters is the spec, the proof files are so large that even finding the spec is not trivial -- in one instance, my browser could hardly handle it. So we should consider if we can clean up those proofs to make them more compact, and/or reorganize the proof files in general so that it is easier to find the specs.