Re: [isabelle] proving a class instantiation.



You misunderstood me. I have not argued that paragraphs should be
indented but that there is an exception to this rule for the first
paragraph - this being another instance of the rule-with-an-exception
pattern. Indeed, your default latex spacing and indenting avoids
excessive and unnecessary indentation. Interestingly avoiding more or
less the indentation pattern you get by the "proper" Isar indentation
rules at the proof level:

lemma
  by

lemma
  by

Tobias

Makarius schrieb:
> 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.