diff -r 0242c9c980df -r a31203f58b20 doc-src/IsarRef/Thy/intro.thy --- a/doc-src/IsarRef/Thy/intro.thy Thu May 08 14:52:07 2008 +0200 +++ b/doc-src/IsarRef/Thy/intro.thy Thu May 08 22:05:15 2008 +0200 @@ -287,10 +287,8 @@ \medskip The present text really is only a reference manual on Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to give some clues of how the concepts introduced here may be put into - practice. \Appref{ap:refcard} provides a quick reference card of - the most common Isabelle/Isar language elements. \Appref{ap:conv} - offers some practical hints on converting existing Isabelle theories - and proof scripts to the new format (without restructuring proofs). + practice. Especially note that \appref{ap:refcard} provides a quick + reference card of the most common Isabelle/Isar language elements. Further issues concerning the Isar concepts are covered in the literature