Default mode of qualifiers in locale commands.

--- a/doc-src/Locales/Locales/Examples.thy	Sat Mar 28 21:07:04 2009 +0100
+++ b/doc-src/Locales/Locales/Examples.thy	Sat Mar 28 22:14:21 2009 +0100
@@ -252,7 +252,8 @@
   additionally outputs the conclusions.
 
   The syntax of the locale commands discussed in this tutorial is
-  shown in Table~\ref{tab:commands}.  See the
+  shown in Table~\ref{tab:commands}.  The grammer is complete with the
+  exception of additional context elements not discussed here.  See the
   Isabelle/Isar Reference Manual~\cite{IsarRef}
   for full documentation.  *}
 

--- a/doc-src/Locales/Locales/Examples1.thy	Sat Mar 28 21:07:04 2009 +0100
+++ b/doc-src/Locales/Locales/Examples1.thy	Sat Mar 28 22:14:21 2009 +0100
@@ -43,13 +43,12 @@
   @{text partial_order} in the global context of the theory.  The
   parameter @{term le} is replaced by @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"}. *} 
 
-  interpretation %visible nat!: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
 txt {* The locale name is succeeded by a \emph{parameter
-  instantiation}.  In general, this is a list of terms, which refer to
+  instantiation}.  This is a list of terms, which refer to
   the parameters in the order of declaration in the locale.  The
-  locale name is preceded by an optional \emph{interpretation prefix},
-  which is used to qualify names from the locale in the global
-  context.
+  locale name is preceded by an optional \emph{interpretation
+  qualifier}.
 
   The command creates the goal%
 \footnote{Note that @{text op} binds tighter than functions
@@ -62,14 +61,12 @@
   interpreted for natural numbers, for example @{thm [source]
   nat.trans}: @{thm [display, indent=2] nat.trans}
 
-  Interpretation accepts a qualifier, @{text nat} in the example,
-  which is applied to all names processed by the interpretation.  If
-  followed by an exclamation point the qualifier is mandatory --- that
-  is, the above theorem cannot be referred to simply by @{text trans}.
-  A qualifier succeeded by an exclamation point is called
-  \emph{strict}.  It prevents unwanted hiding of theorems.  It is
-  advisable to use strict qualifiers for all interpretations in
-  theories.  *}
+  The interpretation qualifier, @{text nat} in the example, is applied
+  to all names processed by the interpretation.  If a qualifer is
+  given in the \isakeyword{interpretation} command, its use is
+  mandatory when referencing the name.  For example, the above theorem
+  cannot be referred to simply by @{text trans}.  This prevents
+  unwanted hiding of theorems. *}
 
 
 subsection {* Second Version: Replacement of Definitions *}

--- a/doc-src/Locales/Locales/Examples2.thy	Sat Mar 28 21:07:04 2009 +0100
+++ b/doc-src/Locales/Locales/Examples2.thy	Sat Mar 28 22:14:21 2009 +0100
@@ -7,7 +7,7 @@
   \isakeyword{where} and require proofs.  The revised command
   that replaces @{text "\<sqsubset>"} by @{text "<"}, is: *}
 
-interpretation %visible nat!: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
+interpretation %visible nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
   where "partial_order.less op \<le> (x::nat) y = (x < y)"
 proof -
   txt {* The goals are @{subgoals [display]}

--- a/doc-src/Locales/Locales/Examples3.thy	Sat Mar 28 21:07:04 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy	Sat Mar 28 22:14:21 2009 +0100
@@ -14,7 +14,7 @@
   \isakeyword{interpret}).  This interpretation is inside the proof of the global
   interpretation.  The third revision of the example illustrates this.  *}
 
-interpretation %visible nat!: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where "partial_order.less op \<le> (x::nat) y = (x < y)"
 proof -
   show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
@@ -48,7 +48,7 @@
   interpretation is reproduced in order to give an example of a more
   elaborate interpretation proof.  *}
 
-interpretation %visible nat!: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where "lattice.meet op \<le> (x::nat) y = min x y"
     and "lattice.join op \<le> (x::nat) y = max x y"
 proof -
@@ -73,7 +73,7 @@
 text {* That the relation @{text \<le>} is a total order completes this
   sequence of interpretations. *}
 
-interpretation %visible nat!: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
   by unfold_locales arith
 
 text {* Theorems that are available in the theory at this point are shown in
@@ -146,7 +146,7 @@
   divisibility.  Instead, interpretation substitutes @{term "x dvd y \<and>
   x \<noteq> y"}.  *}
 
-interpretation nat_dvd!: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
+interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where nat_dvd_meet_eq:
       "lattice.meet op dvd = gcd"
     and nat_dvd_join_eq:
@@ -199,7 +199,7 @@
 lemma %invisible gcd_lcm_distr:
   "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry
 
-interpretation %visible nat_dvd!:
+interpretation %visible nat_dvd:
   distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   apply unfold_locales
   txt {* @{subgoals [display]} *}
@@ -284,11 +284,13 @@
   instances in the order of the sequence.
 
   The qualifiers in the expression are already a familiar concept from
-  the \isakeyword{interpretation} command.  They serve to distinguish
-  names (in particular theorem names) for the two partial orders
-  within the locale.  Qualifiers in the \isakeyword{locale} command
-  default to optional.  Here are examples of theorems in locale @{text
-  order_preserving}: *}
+  the \isakeyword{interpretation} command
+  (Section~\ref{sec:po-first}).  Here, they serve to distinguish names
+  (in particular theorem names) for the two partial orders within the
+  locale.  Qualifiers in the \isakeyword{locale} command (and in
+  \isakeyword{sublocale}) default to optional --- that is, they need
+  not occur in references to the qualified names.  Here are examples
+  of theorems in locale @{text order_preserving}: *}
 
 context %invisible order_preserving begin
 
@@ -359,7 +361,7 @@
 
 text {* In this declaration, the first parameter of @{text
   lattice_hom}, @{text le}, is untouched and then used to instantiate
-  the second parameter.  Its concrete syntax is preseverd. *}
+  the second parameter.  Its concrete syntax is preserved. *}
 
 
 text {* The inheritance diagram of the situation we have now is shown

--- a/doc-src/Locales/Locales/document/Examples.tex	Sat Mar 28 21:07:04 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex	Sat Mar 28 22:14:21 2009 +0100
@@ -481,7 +481,8 @@
   additionally outputs the conclusions.
 
   The syntax of the locale commands discussed in this tutorial is
-  shown in Table~\ref{tab:commands}.  See the
+  shown in Table~\ref{tab:commands}.  The grammer is complete with the
+  exception of additional context elements not discussed here.  See the
   Isabelle/Isar Reference Manual~\cite{IsarRef}
   for full documentation.%
 \end{isamarkuptext}%

--- a/doc-src/Locales/Locales/document/Examples1.tex	Sat Mar 28 21:07:04 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples1.tex	Sat Mar 28 22:14:21 2009 +0100
@@ -72,14 +72,13 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
+\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
 \begin{isamarkuptxt}%
 The locale name is succeeded by a \emph{parameter
-  instantiation}.  In general, this is a list of terms, which refer to
+  instantiation}.  This is a list of terms, which refer to
   the parameters in the order of declaration in the locale.  The
-  locale name is preceded by an optional \emph{interpretation prefix},
-  which is used to qualify names from the locale in the global
-  context.
+  locale name is preceded by an optional \emph{interpretation
+  qualifier}.
 
   The command creates the goal%
 \footnote{Note that \isa{op} binds tighter than functions
@@ -104,14 +103,12 @@
 \ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z%
 \end{isabelle}
 
-  Interpretation accepts a qualifier, \isa{nat} in the example,
-  which is applied to all names processed by the interpretation.  If
-  followed by an exclamation point the qualifier is mandatory --- that
-  is, the above theorem cannot be referred to simply by \isa{trans}.
-  A qualifier succeeded by an exclamation point is called
-  \emph{strict}.  It prevents unwanted hiding of theorems.  It is
-  advisable to use strict qualifiers for all interpretations in
-  theories.%
+  The interpretation qualifier, \isa{nat} in the example, is applied
+  to all names processed by the interpretation.  If a qualifer is
+  given in the \isakeyword{interpretation} command, its use is
+  mandatory when referencing the name.  For example, the above theorem
+  cannot be referred to simply by \isa{trans}.  This prevents
+  unwanted hiding of theorems.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/Locales/Locales/document/Examples2.tex	Sat Mar 28 21:07:04 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples2.tex	Sat Mar 28 22:14:21 2009 +0100
@@ -32,7 +32,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}%

--- a/doc-src/Locales/Locales/document/Examples3.tex	Sat Mar 28 21:07:04 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Sat Mar 28 22:14:21 2009 +0100
@@ -41,7 +41,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharbang}{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
@@ -104,7 +104,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharbang}{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
@@ -174,7 +174,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharbang}{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\ arith%
 \endisatagvisible
@@ -285,7 +285,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharbang}{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\isanewline
 \ \ \ \ \ \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\isanewline
@@ -381,7 +381,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharunderscore}dvd{\isacharbang}{\isacharcolon}\isanewline
+\ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline
 \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{apply}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales%
@@ -493,10 +493,13 @@
   instances in the order of the sequence.
 
   The qualifiers in the expression are already a familiar concept from
-  the \isakeyword{interpretation} command.  They serve to distinguish
-  names (in particular theorem names) for the two partial orders
-  within the locale.  Qualifiers in the \isakeyword{locale} command
-  default to optional.  Here are examples of theorems in locale \isa{order{\isacharunderscore}preserving}:%
+  the \isakeyword{interpretation} command
+  (Section~\ref{sec:po-first}).  Here, they serve to distinguish names
+  (in particular theorem names) for the two partial orders within the
+  locale.  Qualifiers in the \isakeyword{locale} command (and in
+  \isakeyword{sublocale}) default to optional --- that is, they need
+  not occur in references to the qualified names.  Here are examples
+  of theorems in locale \isa{order{\isacharunderscore}preserving}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -610,7 +613,7 @@
 \ lattice{\isacharunderscore}end\ {\isacharequal}\ lattice{\isacharunderscore}hom\ {\isacharunderscore}\ le%
 \begin{isamarkuptext}%
 In this declaration, the first parameter of \isa{lattice{\isacharunderscore}hom}, \isa{le}, is untouched and then used to instantiate
-  the second parameter.  Its concrete syntax is preseverd.%
+  the second parameter.  Its concrete syntax is preserved.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %