added class_deps;
authorwenzelm
Mon, 18 Sep 2006 19:39:14 +0200
changeset 20581 f8cbdf0960ee
parent 20580 6fb75df09253
child 20582 ebd0e03c6a9b
added class_deps;
doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Mon Sep 18 19:39:11 2006 +0200
+++ b/doc-src/IsarRef/pure.tex	Mon Sep 18 19:39:14 2006 +0200
@@ -160,10 +160,12 @@
 \subsection{Type classes and sorts}\label{sec:classes}
 
 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
+\indexisarcmd{class-deps}
 \begin{matharray}{rcll}
   \isarcmd{classes} & : & \isartrans{theory}{theory} \\
   \isarcmd{classrel} & : & \isartrans{theory}{theory} & (axiomatic!) \\
   \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
+  \isarcmd{class_deps} & : & \isarkeep{theory~|~proof} \\
 \end{matharray}
 
 \begin{rail}
@@ -186,6 +188,8 @@
 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
   any type variables given without sort constraints.  Usually, the default
   sort would be only changed when defining a new object-logic.
+\item [$\isarkeyword{class_deps}$] visualizes the subclass relation,
+  using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
 \end{descr}