--- a/doc-src/IsarRef/Thy/document/Introduction.tex Mon Feb 09 12:52:16 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex Mon Feb 09 12:57:05 2009 +0100
@@ -3,8 +3,6 @@
\def\isabellecontext{Introduction}%
%
\isadelimtheory
-\isanewline
-\isanewline
%
\endisadelimtheory
%
@@ -71,11 +69,11 @@
debugging of structured proofs. Isabelle/Isar supports a broad
range of proof styles, both readable and unreadable ones.
- \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}
+ \medskip The generic Isabelle/Isar framework (see
+ \chref{ch:isar-framework}) 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