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