--- a/doc-src/IsarRef/Thy/Introduction.thy Tue Jun 03 00:15:46 2008 +0200
+++ b/doc-src/IsarRef/Thy/Introduction.thy Tue Jun 03 00:16:07 2008 +0200
@@ -51,15 +51,15 @@
debugging of structured proofs. Isabelle/Isar supports a broad
range of proof styles, both readable and unreadable ones.
- \medskip The Isabelle/Isar framework is generic and should work
- reasonably well for any Isabelle object-logic that conforms to the
- natural deduction view of the Isabelle/Pure framework. Specific
- language elements introduced by the major object-logics are
- described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf}
- (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). The main
- language elements are already provided by the Isabelle/Pure
- framework. Nevertheless, examples given in the generic parts will
- usually refer to Isabelle/HOL as well.
+ \medskip The Isabelle/Isar framework \cite{Wenzel:2006:Festschrift}
+ is generic and should work reasonably well for any Isabelle
+ object-logic that conforms to the natural deduction view of the
+ Isabelle/Pure framework. Specific language elements introduced by
+ the major object-logics are described in \chref{ch:hol}
+ (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
+ (Isabelle/ZF). The main language elements are already provided by
+ the Isabelle/Pure framework. Nevertheless, examples given in the
+ generic parts will usually refer to Isabelle/HOL as well.
\medskip Isar commands may be either \emph{proper} document
constructors, or \emph{improper commands}. Some proof methods and