# HG changeset patch
# User wenzelm
# Date 1212444946 -7200
# Node ID ecbe1afe800b8f285ddd604e4d006ee68402a73c
# Parent  4bf8710b3242de74614f79570960130dc3eb131e
updated generated file;

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
diff -r 4bf8710b3242 -r ecbe1afe800b doc-src/IsarRef/Thy/document/Spec.tex
--- 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}