[isabelle] Words in Markus document's, I don't understand

Hi all,

Please, someone can help to understand some words in
http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.pdf ?

Page 27 (printed 12), these words:

  “For example, existing formalizations of linear and modal
   logics simulate sequent-calculus rules within the pure
   natural deduction framework, which would result in slightly
   impractical Isar proof texts.”

Well, I simply don't understand what I quoted above.

What does it mean? An example?

If I ever have other questions from the same document, I will post it in this thread.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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