--- 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
--- a/doc-src/IsarRef/Thy/document/Spec.tex Tue Jun 03 00:05:06 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue Jun 03 00:15:46 2008 +0200
@@ -887,7 +887,7 @@
\indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
\indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\end{matharray}
\begin{rail}