Re: [isabelle] proving a class instantiation.



On Fri, 12 Nov 2010, Tobias Nipkow wrote:

Paragraphs in Ennglish texts are indented, except for the first one in a section.

I did some thorough research on such details before setting a certain default in formal proof documents.

The point of paragraph markup is to emphasize the division of the text. There are two traditions. The one with the indentation and without line spacing is a bit more "anglo saxon" than the other, and more common in software packages from the US. But it is not universal, and fails to achieve its intention with the typical mix of formal and informal parts in Isar documents.

Here is a recent example: http://isabelle.in.tum.de/repos/isabelle/rev/b8d89db3e238 that made a big difference in the clarity of the structure of a text where many paragraphs
are shorter than one line.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.