# HG changeset patch
# User wenzelm
# Date 1212444967 -7200
# Node ID 3dcd890b0bf2a77b36e0a744901a49ef68d7b7c2
# Parent  ecbe1afe800b8f285ddd604e4d006ee68402a73c
\cite{Wenzel:2006:Festschrift};

diff -r ecbe1afe800b -r 3dcd890b0bf2 doc-src/IsarRef/Thy/Introduction.thy
--- 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