--- a/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 21:52:09 2008 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 21:52:59 2008 +0100
@@ -726,9 +726,10 @@
c_class.intro}); this rule is employed by method @{method
intro_classes} to support instantiation proofs of this class.
- The ``class axioms'' are stored as theorems according to the given
- name specifications, adding @{text "c_class"} as name space prefix;
- the same facts are also stored collectively as @{text
+ The ``class axioms'' (which are derived from the internal class
+ definition) are stored as theorems according to the given name
+ specifications; the name space prefix @{text "c_class"} is added
+ here. The full collection of these facts is also stored as @{text
c_class.axioms}.
\item @{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and @{command
@@ -881,7 +882,8 @@
\item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class
@{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}.
- Cyclic class structures are not permitted.
+ Isabelle implicitly maintains the transitive closure of the class
+ hierarchy. Cyclic class structures are not permitted.
\item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
@@ -890,9 +892,17 @@
relations.
\item @{command "defaultsort"}~@{text s} makes sort @{text 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.
+ new default sort for any type variable that is given explicitly in
+ the text, but lacks a sort constraint (wrt.\ the current context).
+ Type variables generated by type inference are not affected.
+
+ Usually the default sort is only changed when defining a new
+ object-logic. For example, the default sort in Isabelle/HOL is
+ @{text type}, the class of all HOL types. %FIXME sort antiq?
+
+ When merging theories, the default sorts of the parents are
+ logically intersected, i.e.\ the representations as lists of classes
+ are joined.
\item @{command "class_deps"} visualizes the subclass relation,
using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
@@ -921,21 +931,23 @@
\begin{description}
- \item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces
- \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for existing type @{text
- "\<tau>"}. Unlike actual type definitions, as are available in
- Isabelle/HOL for example, type synonyms are just purely syntactic
+ \item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
+ \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type
+ @{text "\<tau>"}. Unlike actual type definitions, as are available in
+ Isabelle/HOL for example, type synonyms are merely syntactic
abbreviations without any logical significance. Internally, type
synonyms are fully expanded.
\item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
- type constructor @{text t}, intended as an actual logical type (of
- the object-logic, if available).
+ type constructor @{text t}. If the object-logic defines a base sort
+ @{text s}, then the constructor is declared to operate on that, via
+ the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
+ s) s"}.
\item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n) s"} augments
Isabelle's order-sorted signature of types by new type constructor
arities. This is done axiomatically! The @{command_ref "instance"}
- command (see \S\ref{sec:axclass}) provides a way to introduce proven
+ command (see \secref{sec:axclass}) provides a way to introduce proven
type arities.
\end{description}
@@ -1030,12 +1042,12 @@
message would be issued for any definitional equation with a more
special type than that of the corresponding constant declaration.
- \item @{command "constdefs"} provides a streamlined combination of
- constants declarations and definitions: type-inference takes care of
- the most general typing of the given specification (the optional
- type constraint may refer to type-inference dummies ``@{text _}'' as
- usual). The resulting type declaration needs to agree with that of
- the specification; overloading is \emph{not} supported here!
+ \item @{command "constdefs"} combines constant declarations and
+ definitions, with type-inference taking care of the most general
+ typing of the given specification (the optional type constraint may
+ refer to type-inference dummies ``@{text _}'' as usual). The
+ resulting type declaration needs to agree with that of the
+ specification; overloading is \emph{not} supported here!
The constant name may be omitted altogether, if neither type nor
syntax declarations are given. The canonical name of the
@@ -1047,7 +1059,7 @@
An optional initial context of @{text "(structure)"} declarations
admits use of indexed syntax, using the special symbol @{verbatim
"\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
- particularly useful with locales (see also \S\ref{sec:locale}).
+ particularly useful with locales (see also \secref{sec:locale}).
\end{description}
*}