# HG changeset patch # User wenzelm # Date 1226609579 -3600 # Node ID f09ceb800d00c5649876bb5d80482c8c0dfaf993 # Parent accab7594b8e296a28d289d1c4785d04970500bf minor tuning (according to old ref manual); diff -r accab7594b8e -r f09ceb800d00 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Nov 13 21:52:09 2008 +0100 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Nov 13 21:52:59 2008 +0100 @@ -246,11 +246,11 @@ section {* Mixfix annotations *} text {* Mixfix annotations specify concrete \emph{inner syntax} of - Isabelle types and terms. Some commands such as @{command "types"} - (see \secref{sec:types-pure}) admit infixes only, while @{command - "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see - \secref{sec:syn-trans}) support the full range of general mixfixes - and binders. + Isabelle types and terms. Some commands such as @{command + "typedecl"} admit infixes only, while @{command "definition"} etc.\ + support the full range of general mixfixes and binders. Fixed + parameters in toplevel theorem statements, locale specifications + also admit mixfix annotations. \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} \begin{rail} diff -r accab7594b8e -r f09ceb800d00 doc-src/IsarRef/Thy/Spec.thy --- 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 \ c\<^sub>2"} and @{command @@ -881,7 +882,8 @@ \item @{command "classes"}~@{text "c \ c\<^sub>1, \, c\<^sub>n"} declares class @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \, 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 \ 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 "(\\<^sub>1, \, \\<^sub>n) t = \"} introduces - \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} for existing type @{text - "\"}. Unlike actual type definitions, as are available in - Isabelle/HOL for example, type synonyms are just purely syntactic + \item @{command "types"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"} introduces a + \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} for the existing type + @{text "\"}. 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 "(\\<^sub>1, \, \\<^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, \, + s) s"}. \item @{command "arities"}~@{text "t :: (s\<^sub>1, \, 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 "\"} (printed as ``@{text "\"}''). 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} *}