[isabelle] Words in Markus document's, I don't understand
Please, someone can help to understand some words in
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
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and