--- a/src/Doc/Isar_Ref/HOL_Specific.thy Tue Jul 01 20:47:25 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Tue Jul 01 21:07:02 2014 +0200
@@ -1065,14 +1065,16 @@
produces a type constructor @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} depending on
those type arguments.
- The axiomatization can be considered a ``definition'' in the sense
- of the particular set-theoretic interpretation of HOL
- \cite{pitts93}, where the universe of types is required to be
- downwards-closed wrt.\ arbitrary non-empty subsets. Thus genuinely
- new types introduced by @{command "typedef"} stay within the range
- of HOL models by construction. Note that @{command_ref
- type_synonym} from Isabelle/Pure merely introduces syntactic
- abbreviations, without any logical significance.
+ The axiomatization can be considered a ``definition'' in the sense of the
+ particular set-theoretic interpretation of HOL \cite{pitts93}, where the
+ universe of types is required to be downwards-closed wrt.\ arbitrary
+ non-empty subsets. Thus genuinely new types introduced by @{command
+ "typedef"} stay within the range of HOL models by construction.
+
+ In contrast, the command @{command_ref type_synonym} from Isabelle/Pure
+ merely introduces syntactic abbreviations, without any logical
+ significance. Thus it is more faithful to the idea of a genuine type
+ definition, but less powerful in practice.
@{rail \<open>
@@{command (HOL) typedef} abs_type '=' rep_set
@@ -1084,12 +1086,12 @@
\begin{description}
- \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}
- axiomatizes a type definition in the background theory of the
- current context, depending on a non-emptiness result of the set
- @{text A} that needs to be proven here. The set @{text A} may
- contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} as specified on the LHS,
- but no term variables.
+ \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} produces an
+ axiomatization (\secref{sec:basic-spec}) for a type definition in the
+ background theory of the current context, depending on a non-emptiness
+ result of the set @{text A} that needs to be proven here. The set @{text
+ A} may contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} as specified on the
+ LHS, but no term variables.
Even though a local theory specification, the newly introduced type
constructor cannot depend on parameters or assumptions of the
--- a/src/Doc/Isar_Ref/Spec.thy Tue Jul 01 20:47:25 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Tue Jul 01 21:07:02 2014 +0200
@@ -300,10 +300,15 @@
once and for all, which prevents additional specifications being
issued later on.
- Note that axiomatic specifications are only appropriate when
- declaring a new logical system; axiomatic specifications are
- restricted to global theory contexts. Normal applications should
- only use definitional mechanisms!
+ Axiomatic specifications are required when declaring a new logical system
+ within Isabelle/Pure, but in an application environment like
+ Isabelle/HOL the user normally stays within definitional mechanisms
+ provided by the logic and its libraries.
+
+ Axiomatization is restricted to a global theory context. Despite the
+ possibility to mark some constants as specified by a particular
+ axiomatization, the dependency tracking may be insufficient and disrupt
+ the well-formedness of an otherwise definitional theory.
\item @{command "definition"}~@{text "c \<WHERE> eq"} produces an
internal definition @{text "c \<equiv> t"} according to the specification