Re: [isabelle] proving a class instantiation.



> A marginal question concerning consistency and least surprise: Why do
> many people still indent toplevel Isar proofs differently from local
> ones? E.g. like this:
> 
> lemma foo
> by simp
> 
> instead of the proper form according to the true logical structure of Isar:
> 
> lemma foo
>   by simp

Lambda calculus terms do not need outermost parentheses. Paragraphs in
Ennglish texts are indented, except for the first one in a section. Etc.
For good reasons in each case. And in this case there is not just a
sctructural reason but also the similarity with standard mathematical
practice.

Tobias

> Here the "surprise" has again historical roots, because the first
> version is how unstructured proof scripts would look like, before they
> where manually converted to the new language many years ago.
> 
> 
>     Makarius





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