# HG changeset patch
# User wenzelm
# Date 1404241622 -7200
# Node ID d256f49b4799ceba8ed3e1735fc1d33487cad189
# Parent  08e5c7bc515a5140b3a5eef2348596180d143955
clarified "axiomatization" -- minor rewording of this delicate concept;

diff -r 08e5c7bc515a -r d256f49b4799 src/Doc/Isar_Ref/HOL_Specific.thy
--- 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
diff -r 08e5c7bc515a -r d256f49b4799 src/Doc/Isar_Ref/Spec.thy
--- 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