doc-src/IsarRef/Thy/Spec.thy

 
 section {* Basic specification elements *}
 
 text {*
   \begin{matharray}{rcll}
-    @{command_def "axiomatization"} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
+    @{command_def "axiomatization"} & : & \isarkeep{theory} & (axiomatic!)\\
     @{command_def "definition"} & : & \isarkeep{local{\dsh}theory} \\
     @{attribute_def "defn"} & : & \isaratt \\
     @{command_def "abbreviation"} & : & \isarkeep{local{\dsh}theory} \\
     @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
     @{command_def "notation"} & : & \isarkeep{local{\dsh}theory} \\

   simultaneously and states axiomatic properties for these.  The
   constants are marked as being specified 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.  Normal applications should only use
-  definitional mechanisms!
+  declaring a new logical system; axiomatic specifications are
+  restricted to global theory contexts.  Normal applications should
+  only use definitional mechanisms!
 
   \item [@{command "definition"}~@{text "c \<WHERE> eq"}] produces an
   internal definition @{text "c \<equiv> t"} according to the specification
   given as @{text eq}, which is then turned into a proven fact.  The
   given proposition may deviate from internal meta-level equality