diff -r 4bf8710b3242 -r ecbe1afe800b doc-src/IsarRef/Thy/document/Introduction.tex
--- a/doc-src/IsarRef/Thy/document/Introduction.tex	Tue Jun 03 00:05:06 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex	Tue Jun 03 00:15:46 2008 +0200
@@ -71,15 +71,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