Qualifiers in locale expressions default to mandatory regardless of the command.

--- a/NEWS	Tue Nov 03 18:11:59 2015 +0100
+++ b/NEWS	Wed Nov 04 08:13:49 2015 +0100
@@ -267,6 +267,10 @@
 
 *** Pure ***
 
+* Qualifiers in locale expressions default to mandatory ('!')
+regardless of the command.  Previously, for 'locale' and 'sublocale'
+the default was optional ('?').  INCOMPATIBILITY
+
 * Command 'print_definitions' prints dependencies of definitional
 specifications. This functionality used to be part of 'print_theory'.
 

--- a/src/Doc/Isar_Ref/Spec.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -497,10 +497,8 @@
   If present, the qualifier itself is either optional
   (``\<^verbatim>\<open>?\<close>''), which means that it may be omitted on input of the
   qualified name, or mandatory (``\<^verbatim>\<open>!\<close>'').  If neither
-  ``\<^verbatim>\<open>?\<close>'' nor ``\<^verbatim>\<open>!\<close>'' are present, the command's default
-  is used.  For @{command "interpretation"} and @{command "interpret"}
-  the default is ``mandatory'', for @{command "locale"} and @{command
-  "sublocale"} the default is ``optional''.  Qualifiers play no role
+  ``\<^verbatim>\<open>?\<close>'' nor ``\<^verbatim>\<open>!\<close>'' are present the default
+  is used, which is ``mandatory''.  Qualifiers play no role
   in determining whether one locale instance subsumes another.
 \<close>
 

--- a/src/Doc/Locales/Examples3.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/Doc/Locales/Examples3.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -486,13 +486,13 @@
   proof unfold_locales
     fix f g
     have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)"
-      apply (rule is_infI) apply rule+ apply (drule spec, assumption)+ done
+      apply (rule f.is_infI) apply rule+ apply (drule spec, assumption)+ done
     then show "\<exists>inf. partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g inf"
       by fast
   next
     fix f g
     have "partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<squnion> g x)"
-      apply (rule is_supI) apply rule+ apply (drule spec, assumption)+ done
+      apply (rule f.is_supI) apply rule+ apply (drule spec, assumption)+ done
     then show "\<exists>sup. partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g sup"
       by fast
   qed

--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -298,7 +298,7 @@
 
 section \<open>Interpretation between locales: sublocales\<close>
 
-sublocale lgrp < right: rgrp
+sublocale lgrp < right?: rgrp
 print_facts
 proof unfold_locales
   {
@@ -601,7 +601,7 @@
 lemmas less_thm4 = less_def
 end
 
-locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le
+locale mixin4_combined = le1?: mixin4_mixin le' + le2?: mixin4_copy le for le' le
 begin
 lemmas less_thm4' = less_def
 end
@@ -726,7 +726,7 @@
 
 end
 
-sublocale lgrp < "def": dgrp
+sublocale lgrp < "def"?: dgrp
   where one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
 proof -
   show "dgrp(prod)" by unfold_locales

--- a/src/HOL/Algebra/AbelCoset.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -51,7 +51,7 @@
     kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
       \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
 
-locale abelian_group_hom = G: abelian_group G + H: abelian_group H
+locale abelian_group_hom = G?: abelian_group G + H?: abelian_group H
     for G (structure) and H (structure) +
   fixes h
   assumes a_group_hom: "group_hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>

--- a/src/HOL/Algebra/Group.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -613,7 +613,7 @@
 
 text\<open>Basis for homomorphism proofs: we assume two groups @{term G} and
   @{term H}, with a homomorphism @{term h} between them\<close>
-locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
+locale group_hom = G?: group G + H?: group H for G (structure) and H (structure) +
   fixes h
   assumes homh: "h \<in> hom G H"
 

--- a/src/HOL/Algebra/Lattice.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -925,7 +925,7 @@
 
 text \<open>Total orders are lattices.\<close>
 
-sublocale weak_total_order < weak: weak_lattice
+sublocale weak_total_order < weak?: weak_lattice
 proof
   fix x y
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
@@ -1132,14 +1132,14 @@
   assumes sup_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 
-sublocale upper_semilattice < weak: weak_upper_semilattice
+sublocale upper_semilattice < weak?: weak_upper_semilattice
   by standard (rule sup_of_two_exists)
 
 locale lower_semilattice = partial_order +
   assumes inf_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
 
-sublocale lower_semilattice < weak: weak_lower_semilattice
+sublocale lower_semilattice < weak?: weak_lower_semilattice
   by standard (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
@@ -1190,7 +1190,7 @@
 locale total_order = partial_order +
   assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
 
-sublocale total_order < weak: weak_total_order
+sublocale total_order < weak?: weak_total_order
   by standard (rule total_order_total)
 
 text \<open>Introduction rule: the usual definition of total order\<close>
@@ -1202,7 +1202,7 @@
 
 text \<open>Total orders are lattices.\<close>
 
-sublocale total_order < weak: lattice
+sublocale total_order < weak?: lattice
   by standard (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
@@ -1214,7 +1214,7 @@
     and inf_exists:
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
-sublocale complete_lattice < weak: weak_complete_lattice
+sublocale complete_lattice < weak?: weak_complete_lattice
   by standard (auto intro: sup_exists inf_exists)
 
 text \<open>Introduction rule: the usual definition of complete lattice\<close>

--- a/src/HOL/Algebra/Module.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Algebra/Module.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -14,7 +14,7 @@
 record ('a, 'b) module = "'b ring" +
   smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
 
-locale module = R: cring + M: abelian_group M for M (structure) +
+locale module = R?: cring + M?: abelian_group M for M (structure) +
   assumes smult_closed [simp, intro]:
       "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
     and smult_l_distr:

--- a/src/HOL/Algebra/Ring.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Algebra/Ring.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -648,7 +648,7 @@
   shows "h \<in> ring_hom R S ==> h \<one> = \<one>\<^bsub>S\<^esub>"
   by (simp add: ring_hom_def)
 
-locale ring_hom_cring = R: cring R + S: cring S
+locale ring_hom_cring = R?: cring R + S?: cring S
     for R (structure) and S (structure) +
   fixes h
   assumes homh [simp, intro]: "h \<in> ring_hom R S"

--- a/src/HOL/Algebra/RingHom.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -9,7 +9,7 @@
 section \<open>Homomorphisms of Non-Commutative Rings\<close>
 
 text \<open>Lifting existing lemmas in a @{text ring_hom_ring} locale\<close>
-locale ring_hom_ring = R: ring R + S: ring S
+locale ring_hom_ring = R?: ring R + S?: ring S
     for R (structure) and S (structure) +
   fixes h
   assumes homh: "h \<in> ring_hom R S"
@@ -19,7 +19,7 @@
 sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
   by standard (rule homh)
 
-sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
+sublocale ring_hom_ring \<subseteq> abelian_group?: abelian_group_hom R S
 apply (rule abelian_group_homI)
   apply (rule R.is_abelian_group)
  apply (rule S.is_abelian_group)

--- a/src/HOL/Algebra/UnivPoly.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -174,14 +174,14 @@
   fixes R (structure) and P (structure)
   defines P_def: "P == UP R"
 
-locale UP_ring = UP + R: ring R
+locale UP_ring = UP + R?: ring R
 
-locale UP_cring = UP + R: cring R
+locale UP_cring = UP + R?: cring R
 
 sublocale UP_cring < UP_ring
   by intro_locales [1] (rule P_def)
 
-locale UP_domain = UP + R: "domain" R
+locale UP_domain = UP + R?: "domain" R
 
 sublocale UP_domain < UP_cring
   by intro_locales [1] (rule P_def)
@@ -457,8 +457,8 @@
 
 end
 
-sublocale UP_ring < P: ring P using UP_ring .
-sublocale UP_cring < P: cring P using UP_cring .
+sublocale UP_ring < P?: ring P using UP_ring .
+sublocale UP_cring < P?: cring P using UP_cring .
 
 
 subsection \<open>Polynomials Form an Algebra\<close>
@@ -1196,8 +1196,6 @@
 
 locale UP_pre_univ_prop = ring_hom_cring + UP_cring
 
-(* FIXME print_locale ring_hom_cring fails *)
-
 locale UP_univ_prop = UP_pre_univ_prop +
   fixes s and Eval
   assumes indet_img_carrier [simp, intro]: "s \<in> carrier S"

--- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -322,7 +322,7 @@
 
 subsection {* Binary products of $\sigma$-finite emeasure spaces *}
 
-locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2
+locale pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2
   for M1 :: "'a measure" and M2 :: "'b measure"
 
 lemma (in pair_sigma_finite) measurable_emeasure_Pair1:
@@ -379,7 +379,7 @@
   qed
 qed
 
-sublocale pair_sigma_finite \<subseteq> P: sigma_finite_measure "M1 \<Otimes>\<^sub>M M2"
+sublocale pair_sigma_finite \<subseteq> P?: sigma_finite_measure "M1 \<Otimes>\<^sub>M M2"
 proof
   from M1.sigma_finite_countable guess F1 ..
   moreover from M2.sigma_finite_countable guess F2 ..

--- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -829,7 +829,7 @@
   fixes M :: "'i \<Rightarrow> 'a measure"
   assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
 
-sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
+sublocale product_sigma_finite \<subseteq> M?: sigma_finite_measure "M i" for i
   by (rule sigma_finite_measures)
 
 locale finite_product_sigma_finite = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +

--- a/src/HOL/Probability/Giry_Monad.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -133,7 +133,7 @@
 locale pair_subprob_space = 
   pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
 
-sublocale pair_subprob_space \<subseteq> P: subprob_space "M1 \<Otimes>\<^sub>M M2"
+sublocale pair_subprob_space \<subseteq> P?: subprob_space "M1 \<Otimes>\<^sub>M M2"
 proof
   have "\<And>a b. \<lbrakk>a \<ge> 0; b \<ge> 0; a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a * b \<le> (1::ereal)"
     by (metis monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono)

--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -51,7 +51,7 @@
     emeasure (Pi\<^sub>M I M) (emb I J (Pi\<^sub>E J X)) = (\<Prod> i\<in>J. emeasure (M i) (X i))"
   by (subst emeasure_PiM_emb') (auto intro!: emeasure_PiM)
 
-sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^sub>M I M"
+sublocale product_prob_space \<subseteq> P?: prob_space "Pi\<^sub>M I M"
 proof
   have *: "emb I {} {\<lambda>x. undefined} = space (PiM I M)"
     by (auto simp: prod_emb_def space_PiM)

--- a/src/HOL/Probability/Probability_Measure.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -461,7 +461,7 @@
 
 locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
 
-sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^sub>M M2"
+sublocale pair_prob_space \<subseteq> P?: prob_space "M1 \<Otimes>\<^sub>M M2"
 proof
   show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) = 1"
     by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
@@ -471,7 +471,7 @@
   fixes I :: "'i set"
   assumes prob_space: "\<And>i. prob_space (M i)"
 
-sublocale product_prob_space \<subseteq> M: prob_space "M i" for i
+sublocale product_prob_space \<subseteq> M?: prob_space "M i" for i
   by (rule prob_space)
 
 locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I

--- a/src/HOL/ex/LocaleTest2.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -826,7 +826,7 @@
 proof -
   have "hom one +++ zero = hom one +++ hom one"
     by (simp add: hom_mult [symmetric] del: hom_mult)
-  then show ?thesis by (simp del: r_one)
+  then show ?thesis by (simp del: sum.r_one)
 qed
 
 end

--- a/src/HOL/ex/Tarski.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/ex/Tarski.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -119,7 +119,7 @@
 locale CL = S +
   assumes cl_co:  "cl : CompleteLattice"
 
-sublocale CL < po: PO
+sublocale CL < po?: PO
 apply (simp_all add: A_def r_def)
 apply unfold_locales
 using cl_co unfolding CompleteLattice_def by auto
@@ -130,7 +130,7 @@
   assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
   defines P_def: "P == fix f A"
 
-sublocale CLF < cl: CL
+sublocale CLF < cl?: CL
 apply (simp_all add: A_def r_def)
 apply unfold_locales
 using f_cl unfolding CLF_set_def by auto

--- a/src/Pure/Isar/isar_syn.ML	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 04 08:13:49 2015 +0100
@@ -384,7 +384,7 @@
 (* locales *)
 
 val locale_val =
-  Parse_Spec.locale_expression false --
+  Parse_Spec.locale_expression true --
     Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
 
@@ -402,8 +402,8 @@
       >> (fn elems =>
           Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
 
-fun interpretation_args mandatory =
-  Parse.!!! (Parse_Spec.locale_expression mandatory) --
+val interpretation_args =
+  Parse.!!! (Parse_Spec.locale_expression true) --
     Scan.optional
       (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
 
@@ -411,21 +411,21 @@
   Outer_Syntax.command @{command_keyword sublocale}
     "prove sublocale relation between a locale and a locale expression"
     ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
-      interpretation_args false >> (fn (loc, (expr, equations)) =>
+      interpretation_args >> (fn (loc, (expr, equations)) =>
         Toplevel.theory_to_proof (Expression.sublocale_global_cmd loc expr equations)))
-    || interpretation_args false >> (fn (expr, equations) =>
+    || interpretation_args >> (fn (expr, equations) =>
         Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
 
 val _ =
   Outer_Syntax.command @{command_keyword interpretation}
     "prove interpretation of locale expression in local theory"
-    (interpretation_args true >> (fn (expr, equations) =>
+    (interpretation_args >> (fn (expr, equations) =>
       Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
 
 val _ =
   Outer_Syntax.command @{command_keyword interpret}
     "prove interpretation of locale expression in proof context"
-    (interpretation_args true >> (fn (expr, equations) =>
+    (interpretation_args >> (fn (expr, equations) =>
       Toplevel.proof' (Expression.interpret_cmd expr equations)));
 
 

--- a/src/ZF/ex/Group.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/ZF/ex/Group.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -429,7 +429,7 @@
 proof -
   have "h ` \<one> \<cdot>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = (h ` \<one>) \<cdot>\<^bsub>H\<^esub> (h ` \<one>)"
     by (simp add: hom_mult [symmetric] del: hom_mult)
-  then show ?thesis by (simp del: r_one)
+  then show ?thesis by (simp del: H.r_one)
 qed
 
 lemma (in group_hom) inv_closed [simp]:
@@ -445,7 +445,7 @@
   also from x have "... = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)"
     by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
   finally have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)" .
-  with x show ?thesis by (simp del: inv)
+  with x show ?thesis by (simp del: H.inv)
 qed
 
 subsection \<open>Commutative Structures\<close>
@@ -596,7 +596,7 @@
   "set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
 
 
-locale normal = subgroup: subgroup + group +
+locale normal = subgroup + group +
   assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
 
 notation