Qualifiers in locale expressions default to mandatory regardless of the command.
authorballarin
Wed Nov 04 08:13:49 2015 +0100 (2015-11-04)
changeset 61565352c73a689da
parent 61564 6d513469f9b2
child 61566 c3d6e570ccef
Qualifiers in locale expressions default to mandatory regardless of the command.
NEWS
src/Doc/Isar_Ref/Spec.thy
src/Doc/Locales/Examples3.thy
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/ex/LocaleTest2.thy
src/HOL/ex/Tarski.thy
src/Pure/Isar/isar_syn.ML
src/ZF/ex/Group.thy
     1.1 --- a/NEWS	Tue Nov 03 18:11:59 2015 +0100
     1.2 +++ b/NEWS	Wed Nov 04 08:13:49 2015 +0100
     1.3 @@ -267,6 +267,10 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Qualifiers in locale expressions default to mandatory ('!')
     1.8 +regardless of the command.  Previously, for 'locale' and 'sublocale'
     1.9 +the default was optional ('?').  INCOMPATIBILITY
    1.10 +
    1.11  * Command 'print_definitions' prints dependencies of definitional
    1.12  specifications. This functionality used to be part of 'print_theory'.
    1.13  
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Tue Nov 03 18:11:59 2015 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Wed Nov 04 08:13:49 2015 +0100
     2.3 @@ -497,10 +497,8 @@
     2.4    If present, the qualifier itself is either optional
     2.5    (``\<^verbatim>\<open>?\<close>''), which means that it may be omitted on input of the
     2.6    qualified name, or mandatory (``\<^verbatim>\<open>!\<close>'').  If neither
     2.7 -  ``\<^verbatim>\<open>?\<close>'' nor ``\<^verbatim>\<open>!\<close>'' are present, the command's default
     2.8 -  is used.  For @{command "interpretation"} and @{command "interpret"}
     2.9 -  the default is ``mandatory'', for @{command "locale"} and @{command
    2.10 -  "sublocale"} the default is ``optional''.  Qualifiers play no role
    2.11 +  ``\<^verbatim>\<open>?\<close>'' nor ``\<^verbatim>\<open>!\<close>'' are present the default
    2.12 +  is used, which is ``mandatory''.  Qualifiers play no role
    2.13    in determining whether one locale instance subsumes another.
    2.14  \<close>
    2.15  
     3.1 --- a/src/Doc/Locales/Examples3.thy	Tue Nov 03 18:11:59 2015 +0100
     3.2 +++ b/src/Doc/Locales/Examples3.thy	Wed Nov 04 08:13:49 2015 +0100
     3.3 @@ -486,13 +486,13 @@
     3.4    proof unfold_locales
     3.5      fix f g
     3.6      have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)"
     3.7 -      apply (rule is_infI) apply rule+ apply (drule spec, assumption)+ done
     3.8 +      apply (rule f.is_infI) apply rule+ apply (drule spec, assumption)+ done
     3.9      then show "\<exists>inf. partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g inf"
    3.10        by fast
    3.11    next
    3.12      fix f g
    3.13      have "partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<squnion> g x)"
    3.14 -      apply (rule is_supI) apply rule+ apply (drule spec, assumption)+ done
    3.15 +      apply (rule f.is_supI) apply rule+ apply (drule spec, assumption)+ done
    3.16      then show "\<exists>sup. partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g sup"
    3.17        by fast
    3.18    qed
     4.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Tue Nov 03 18:11:59 2015 +0100
     4.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Nov 04 08:13:49 2015 +0100
     4.3 @@ -298,7 +298,7 @@
     4.4  
     4.5  section \<open>Interpretation between locales: sublocales\<close>
     4.6  
     4.7 -sublocale lgrp < right: rgrp
     4.8 +sublocale lgrp < right?: rgrp
     4.9  print_facts
    4.10  proof unfold_locales
    4.11    {
    4.12 @@ -601,7 +601,7 @@
    4.13  lemmas less_thm4 = less_def
    4.14  end
    4.15  
    4.16 -locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le
    4.17 +locale mixin4_combined = le1?: mixin4_mixin le' + le2?: mixin4_copy le for le' le
    4.18  begin
    4.19  lemmas less_thm4' = less_def
    4.20  end
    4.21 @@ -726,7 +726,7 @@
    4.22  
    4.23  end
    4.24  
    4.25 -sublocale lgrp < "def": dgrp
    4.26 +sublocale lgrp < "def"?: dgrp
    4.27    where one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
    4.28  proof -
    4.29    show "dgrp(prod)" by unfold_locales
     5.1 --- a/src/HOL/Algebra/AbelCoset.thy	Tue Nov 03 18:11:59 2015 +0100
     5.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Wed Nov 04 08:13:49 2015 +0100
     5.3 @@ -51,7 +51,7 @@
     5.4      kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
     5.5        \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
     5.6  
     5.7 -locale abelian_group_hom = G: abelian_group G + H: abelian_group H
     5.8 +locale abelian_group_hom = G?: abelian_group G + H?: abelian_group H
     5.9      for G (structure) and H (structure) +
    5.10    fixes h
    5.11    assumes a_group_hom: "group_hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
     6.1 --- a/src/HOL/Algebra/Group.thy	Tue Nov 03 18:11:59 2015 +0100
     6.2 +++ b/src/HOL/Algebra/Group.thy	Wed Nov 04 08:13:49 2015 +0100
     6.3 @@ -613,7 +613,7 @@
     6.4  
     6.5  text\<open>Basis for homomorphism proofs: we assume two groups @{term G} and
     6.6    @{term H}, with a homomorphism @{term h} between them\<close>
     6.7 -locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
     6.8 +locale group_hom = G?: group G + H?: group H for G (structure) and H (structure) +
     6.9    fixes h
    6.10    assumes homh: "h \<in> hom G H"
    6.11  
     7.1 --- a/src/HOL/Algebra/Lattice.thy	Tue Nov 03 18:11:59 2015 +0100
     7.2 +++ b/src/HOL/Algebra/Lattice.thy	Wed Nov 04 08:13:49 2015 +0100
     7.3 @@ -925,7 +925,7 @@
     7.4  
     7.5  text \<open>Total orders are lattices.\<close>
     7.6  
     7.7 -sublocale weak_total_order < weak: weak_lattice
     7.8 +sublocale weak_total_order < weak?: weak_lattice
     7.9  proof
    7.10    fix x y
    7.11    assume L: "x \<in> carrier L"  "y \<in> carrier L"
    7.12 @@ -1132,14 +1132,14 @@
    7.13    assumes sup_of_two_exists:
    7.14      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
    7.15  
    7.16 -sublocale upper_semilattice < weak: weak_upper_semilattice
    7.17 +sublocale upper_semilattice < weak?: weak_upper_semilattice
    7.18    by standard (rule sup_of_two_exists)
    7.19  
    7.20  locale lower_semilattice = partial_order +
    7.21    assumes inf_of_two_exists:
    7.22      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
    7.23  
    7.24 -sublocale lower_semilattice < weak: weak_lower_semilattice
    7.25 +sublocale lower_semilattice < weak?: weak_lower_semilattice
    7.26    by standard (rule inf_of_two_exists)
    7.27  
    7.28  locale lattice = upper_semilattice + lower_semilattice
    7.29 @@ -1190,7 +1190,7 @@
    7.30  locale total_order = partial_order +
    7.31    assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
    7.32  
    7.33 -sublocale total_order < weak: weak_total_order
    7.34 +sublocale total_order < weak?: weak_total_order
    7.35    by standard (rule total_order_total)
    7.36  
    7.37  text \<open>Introduction rule: the usual definition of total order\<close>
    7.38 @@ -1202,7 +1202,7 @@
    7.39  
    7.40  text \<open>Total orders are lattices.\<close>
    7.41  
    7.42 -sublocale total_order < weak: lattice
    7.43 +sublocale total_order < weak?: lattice
    7.44    by standard (auto intro: sup_of_two_exists inf_of_two_exists)
    7.45  
    7.46  
    7.47 @@ -1214,7 +1214,7 @@
    7.48      and inf_exists:
    7.49      "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    7.50  
    7.51 -sublocale complete_lattice < weak: weak_complete_lattice
    7.52 +sublocale complete_lattice < weak?: weak_complete_lattice
    7.53    by standard (auto intro: sup_exists inf_exists)
    7.54  
    7.55  text \<open>Introduction rule: the usual definition of complete lattice\<close>
     8.1 --- a/src/HOL/Algebra/Module.thy	Tue Nov 03 18:11:59 2015 +0100
     8.2 +++ b/src/HOL/Algebra/Module.thy	Wed Nov 04 08:13:49 2015 +0100
     8.3 @@ -14,7 +14,7 @@
     8.4  record ('a, 'b) module = "'b ring" +
     8.5    smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
     8.6  
     8.7 -locale module = R: cring + M: abelian_group M for M (structure) +
     8.8 +locale module = R?: cring + M?: abelian_group M for M (structure) +
     8.9    assumes smult_closed [simp, intro]:
    8.10        "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
    8.11      and smult_l_distr:
     9.1 --- a/src/HOL/Algebra/Ring.thy	Tue Nov 03 18:11:59 2015 +0100
     9.2 +++ b/src/HOL/Algebra/Ring.thy	Wed Nov 04 08:13:49 2015 +0100
     9.3 @@ -648,7 +648,7 @@
     9.4    shows "h \<in> ring_hom R S ==> h \<one> = \<one>\<^bsub>S\<^esub>"
     9.5    by (simp add: ring_hom_def)
     9.6  
     9.7 -locale ring_hom_cring = R: cring R + S: cring S
     9.8 +locale ring_hom_cring = R?: cring R + S?: cring S
     9.9      for R (structure) and S (structure) +
    9.10    fixes h
    9.11    assumes homh [simp, intro]: "h \<in> ring_hom R S"
    10.1 --- a/src/HOL/Algebra/RingHom.thy	Tue Nov 03 18:11:59 2015 +0100
    10.2 +++ b/src/HOL/Algebra/RingHom.thy	Wed Nov 04 08:13:49 2015 +0100
    10.3 @@ -9,7 +9,7 @@
    10.4  section \<open>Homomorphisms of Non-Commutative Rings\<close>
    10.5  
    10.6  text \<open>Lifting existing lemmas in a @{text ring_hom_ring} locale\<close>
    10.7 -locale ring_hom_ring = R: ring R + S: ring S
    10.8 +locale ring_hom_ring = R?: ring R + S?: ring S
    10.9      for R (structure) and S (structure) +
   10.10    fixes h
   10.11    assumes homh: "h \<in> ring_hom R S"
   10.12 @@ -19,7 +19,7 @@
   10.13  sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
   10.14    by standard (rule homh)
   10.15  
   10.16 -sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
   10.17 +sublocale ring_hom_ring \<subseteq> abelian_group?: abelian_group_hom R S
   10.18  apply (rule abelian_group_homI)
   10.19    apply (rule R.is_abelian_group)
   10.20   apply (rule S.is_abelian_group)
    11.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Nov 03 18:11:59 2015 +0100
    11.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Nov 04 08:13:49 2015 +0100
    11.3 @@ -174,14 +174,14 @@
    11.4    fixes R (structure) and P (structure)
    11.5    defines P_def: "P == UP R"
    11.6  
    11.7 -locale UP_ring = UP + R: ring R
    11.8 +locale UP_ring = UP + R?: ring R
    11.9  
   11.10 -locale UP_cring = UP + R: cring R
   11.11 +locale UP_cring = UP + R?: cring R
   11.12  
   11.13  sublocale UP_cring < UP_ring
   11.14    by intro_locales [1] (rule P_def)
   11.15  
   11.16 -locale UP_domain = UP + R: "domain" R
   11.17 +locale UP_domain = UP + R?: "domain" R
   11.18  
   11.19  sublocale UP_domain < UP_cring
   11.20    by intro_locales [1] (rule P_def)
   11.21 @@ -457,8 +457,8 @@
   11.22  
   11.23  end
   11.24  
   11.25 -sublocale UP_ring < P: ring P using UP_ring .
   11.26 -sublocale UP_cring < P: cring P using UP_cring .
   11.27 +sublocale UP_ring < P?: ring P using UP_ring .
   11.28 +sublocale UP_cring < P?: cring P using UP_cring .
   11.29  
   11.30  
   11.31  subsection \<open>Polynomials Form an Algebra\<close>
   11.32 @@ -1196,8 +1196,6 @@
   11.33  
   11.34  locale UP_pre_univ_prop = ring_hom_cring + UP_cring
   11.35  
   11.36 -(* FIXME print_locale ring_hom_cring fails *)
   11.37 -
   11.38  locale UP_univ_prop = UP_pre_univ_prop +
   11.39    fixes s and Eval
   11.40    assumes indet_img_carrier [simp, intro]: "s \<in> carrier S"
    12.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Nov 03 18:11:59 2015 +0100
    12.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Nov 04 08:13:49 2015 +0100
    12.3 @@ -322,7 +322,7 @@
    12.4  
    12.5  subsection {* Binary products of $\sigma$-finite emeasure spaces *}
    12.6  
    12.7 -locale pair_sigma_finite = M1: sigma_finite_measure M1 + M2: sigma_finite_measure M2
    12.8 +locale pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2
    12.9    for M1 :: "'a measure" and M2 :: "'b measure"
   12.10  
   12.11  lemma (in pair_sigma_finite) measurable_emeasure_Pair1:
   12.12 @@ -379,7 +379,7 @@
   12.13    qed
   12.14  qed
   12.15  
   12.16 -sublocale pair_sigma_finite \<subseteq> P: sigma_finite_measure "M1 \<Otimes>\<^sub>M M2"
   12.17 +sublocale pair_sigma_finite \<subseteq> P?: sigma_finite_measure "M1 \<Otimes>\<^sub>M M2"
   12.18  proof
   12.19    from M1.sigma_finite_countable guess F1 ..
   12.20    moreover from M2.sigma_finite_countable guess F2 ..
    13.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 03 18:11:59 2015 +0100
    13.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Nov 04 08:13:49 2015 +0100
    13.3 @@ -829,7 +829,7 @@
    13.4    fixes M :: "'i \<Rightarrow> 'a measure"
    13.5    assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
    13.6  
    13.7 -sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
    13.8 +sublocale product_sigma_finite \<subseteq> M?: sigma_finite_measure "M i" for i
    13.9    by (rule sigma_finite_measures)
   13.10  
   13.11  locale finite_product_sigma_finite = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
    14.1 --- a/src/HOL/Probability/Giry_Monad.thy	Tue Nov 03 18:11:59 2015 +0100
    14.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Wed Nov 04 08:13:49 2015 +0100
    14.3 @@ -133,7 +133,7 @@
    14.4  locale pair_subprob_space = 
    14.5    pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
    14.6  
    14.7 -sublocale pair_subprob_space \<subseteq> P: subprob_space "M1 \<Otimes>\<^sub>M M2"
    14.8 +sublocale pair_subprob_space \<subseteq> P?: subprob_space "M1 \<Otimes>\<^sub>M M2"
    14.9  proof
   14.10    have "\<And>a b. \<lbrakk>a \<ge> 0; b \<ge> 0; a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a * b \<le> (1::ereal)"
   14.11      by (metis monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono)
    15.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Nov 03 18:11:59 2015 +0100
    15.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Nov 04 08:13:49 2015 +0100
    15.3 @@ -51,7 +51,7 @@
    15.4      emeasure (Pi\<^sub>M I M) (emb I J (Pi\<^sub>E J X)) = (\<Prod> i\<in>J. emeasure (M i) (X i))"
    15.5    by (subst emeasure_PiM_emb') (auto intro!: emeasure_PiM)
    15.6  
    15.7 -sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^sub>M I M"
    15.8 +sublocale product_prob_space \<subseteq> P?: prob_space "Pi\<^sub>M I M"
    15.9  proof
   15.10    have *: "emb I {} {\<lambda>x. undefined} = space (PiM I M)"
   15.11      by (auto simp: prod_emb_def space_PiM)
    16.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue Nov 03 18:11:59 2015 +0100
    16.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Wed Nov 04 08:13:49 2015 +0100
    16.3 @@ -461,7 +461,7 @@
    16.4  
    16.5  locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
    16.6  
    16.7 -sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^sub>M M2"
    16.8 +sublocale pair_prob_space \<subseteq> P?: prob_space "M1 \<Otimes>\<^sub>M M2"
    16.9  proof
   16.10    show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) = 1"
   16.11      by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
   16.12 @@ -471,7 +471,7 @@
   16.13    fixes I :: "'i set"
   16.14    assumes prob_space: "\<And>i. prob_space (M i)"
   16.15  
   16.16 -sublocale product_prob_space \<subseteq> M: prob_space "M i" for i
   16.17 +sublocale product_prob_space \<subseteq> M?: prob_space "M i" for i
   16.18    by (rule prob_space)
   16.19  
   16.20  locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I
    17.1 --- a/src/HOL/ex/LocaleTest2.thy	Tue Nov 03 18:11:59 2015 +0100
    17.2 +++ b/src/HOL/ex/LocaleTest2.thy	Wed Nov 04 08:13:49 2015 +0100
    17.3 @@ -826,7 +826,7 @@
    17.4  proof -
    17.5    have "hom one +++ zero = hom one +++ hom one"
    17.6      by (simp add: hom_mult [symmetric] del: hom_mult)
    17.7 -  then show ?thesis by (simp del: r_one)
    17.8 +  then show ?thesis by (simp del: sum.r_one)
    17.9  qed
   17.10  
   17.11  end
    18.1 --- a/src/HOL/ex/Tarski.thy	Tue Nov 03 18:11:59 2015 +0100
    18.2 +++ b/src/HOL/ex/Tarski.thy	Wed Nov 04 08:13:49 2015 +0100
    18.3 @@ -119,7 +119,7 @@
    18.4  locale CL = S +
    18.5    assumes cl_co:  "cl : CompleteLattice"
    18.6  
    18.7 -sublocale CL < po: PO
    18.8 +sublocale CL < po?: PO
    18.9  apply (simp_all add: A_def r_def)
   18.10  apply unfold_locales
   18.11  using cl_co unfolding CompleteLattice_def by auto
   18.12 @@ -130,7 +130,7 @@
   18.13    assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
   18.14    defines P_def: "P == fix f A"
   18.15  
   18.16 -sublocale CLF < cl: CL
   18.17 +sublocale CLF < cl?: CL
   18.18  apply (simp_all add: A_def r_def)
   18.19  apply unfold_locales
   18.20  using f_cl unfolding CLF_set_def by auto
    19.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Nov 03 18:11:59 2015 +0100
    19.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 04 08:13:49 2015 +0100
    19.3 @@ -384,7 +384,7 @@
    19.4  (* locales *)
    19.5  
    19.6  val locale_val =
    19.7 -  Parse_Spec.locale_expression false --
    19.8 +  Parse_Spec.locale_expression true --
    19.9      Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   19.10    Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
   19.11  
   19.12 @@ -402,8 +402,8 @@
   19.13        >> (fn elems =>
   19.14            Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
   19.15  
   19.16 -fun interpretation_args mandatory =
   19.17 -  Parse.!!! (Parse_Spec.locale_expression mandatory) --
   19.18 +val interpretation_args =
   19.19 +  Parse.!!! (Parse_Spec.locale_expression true) --
   19.20      Scan.optional
   19.21        (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
   19.22  
   19.23 @@ -411,21 +411,21 @@
   19.24    Outer_Syntax.command @{command_keyword sublocale}
   19.25      "prove sublocale relation between a locale and a locale expression"
   19.26      ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
   19.27 -      interpretation_args false >> (fn (loc, (expr, equations)) =>
   19.28 +      interpretation_args >> (fn (loc, (expr, equations)) =>
   19.29          Toplevel.theory_to_proof (Expression.sublocale_global_cmd loc expr equations)))
   19.30 -    || interpretation_args false >> (fn (expr, equations) =>
   19.31 +    || interpretation_args >> (fn (expr, equations) =>
   19.32          Toplevel.local_theory_to_proof NONE NONE (Expression.sublocale_cmd expr equations)));
   19.33  
   19.34  val _ =
   19.35    Outer_Syntax.command @{command_keyword interpretation}
   19.36      "prove interpretation of locale expression in local theory"
   19.37 -    (interpretation_args true >> (fn (expr, equations) =>
   19.38 +    (interpretation_args >> (fn (expr, equations) =>
   19.39        Toplevel.local_theory_to_proof NONE NONE (Expression.interpretation_cmd expr equations)));
   19.40  
   19.41  val _ =
   19.42    Outer_Syntax.command @{command_keyword interpret}
   19.43      "prove interpretation of locale expression in proof context"
   19.44 -    (interpretation_args true >> (fn (expr, equations) =>
   19.45 +    (interpretation_args >> (fn (expr, equations) =>
   19.46        Toplevel.proof' (Expression.interpret_cmd expr equations)));
   19.47  
   19.48  
    20.1 --- a/src/ZF/ex/Group.thy	Tue Nov 03 18:11:59 2015 +0100
    20.2 +++ b/src/ZF/ex/Group.thy	Wed Nov 04 08:13:49 2015 +0100
    20.3 @@ -429,7 +429,7 @@
    20.4  proof -
    20.5    have "h ` \<one> \<cdot>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = (h ` \<one>) \<cdot>\<^bsub>H\<^esub> (h ` \<one>)"
    20.6      by (simp add: hom_mult [symmetric] del: hom_mult)
    20.7 -  then show ?thesis by (simp del: r_one)
    20.8 +  then show ?thesis by (simp del: H.r_one)
    20.9  qed
   20.10  
   20.11  lemma (in group_hom) inv_closed [simp]:
   20.12 @@ -445,7 +445,7 @@
   20.13    also from x have "... = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)"
   20.14      by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
   20.15    finally have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)" .
   20.16 -  with x show ?thesis by (simp del: inv)
   20.17 +  with x show ?thesis by (simp del: H.inv)
   20.18  qed
   20.19  
   20.20  subsection \<open>Commutative Structures\<close>
   20.21 @@ -596,7 +596,7 @@
   20.22    "set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
   20.23  
   20.24  
   20.25 -locale normal = subgroup: subgroup + group +
   20.26 +locale normal = subgroup + group +
   20.27    assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
   20.28  
   20.29  notation