# HG changeset patch
# User ballarin
# Date 1446621232 -3600
# Node ID c3d6e570ccefff8d6add2f945ad7fdf81e0bd432
# Parent  352c73a689da255bd1c202bd4e0a2ac66b52abcc
Keyword 'rewrites' identifies rewrite morphisms.

diff -r 352c73a689da -r c3d6e570ccef NEWS
--- a/NEWS	Wed Nov 04 08:13:49 2015 +0100
+++ b/NEWS	Wed Nov 04 08:13:52 2015 +0100
@@ -271,6 +271,9 @@
 regardless of the command.  Previously, for 'locale' and 'sublocale'
 the default was optional ('?').  INCOMPATIBILITY
 
+* Keyword 'rewrites' identifies rewrite morphisms in interpretation
+commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY
+
 * Command 'print_definitions' prints dependencies of definitional
 specifications. This functionality used to be part of 'print_theory'.
 
diff -r 352c73a689da -r c3d6e570ccef src/Doc/Classes/Classes.thy
--- a/src/Doc/Classes/Classes.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Classes/Classes.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -457,7 +457,7 @@
   "replicate 0 _ = []"
   | "replicate (Suc n) xs = xs @ replicate n xs"
 
-interpretation %quote list_monoid: monoid append "[]" where
+interpretation %quote list_monoid: monoid append "[]" rewrites
   "monoid.pow_nat append [] = replicate"
 proof -
   interpret monoid append "[]" ..
diff -r 352c73a689da -r c3d6e570ccef src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Codegen/Further.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -202,7 +202,7 @@
   The interpretation itself is enriched with an equation @{text "t = c"}:
 \<close>
 
-interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)" where
+interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)" rewrites
   "power.powers (\<lambda>n f. f ^^ n) = funpows"
   by unfold_locales
     (simp_all add: fun_eq_iff funpow_mult mult.commute funpows_def)
diff -r 352c73a689da -r c3d6e570ccef src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -676,10 +676,10 @@
     @@{command print_interps} @{syntax nameref}
     ;
 
-    equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
+    equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
   \<close>}
 
-  \<^descr> @{command "interpretation"}~\<open>expr \<WHERE> eqns\<close>
+  \<^descr> @{command "interpretation"}~\<open>expr\<close>~@{keyword "rewrites"}~\<open>eqns\<close>
   interprets \<open>expr\<close> in a global or local theory.  The command
   generates proof obligations for the instantiated specifications.
   Once these are discharged by the user, instantiated declarations (in
@@ -720,14 +720,13 @@
   concepts introduced through definitions.  The equations must be
   proved.
 
-  \<^descr> @{command "interpret"}~\<open>expr \<WHERE> eqns\<close> interprets
+  \<^descr> @{command "interpret"}~\<open>expr\<close>~@{keyword "rewrites"}~\<open>eqns\<close> interprets
   \<open>expr\<close> in the proof context and is otherwise similar to
   interpretation in local theories.  Note that for @{command
   "interpret"} the \<open>eqns\<close> should be
   explicitly universally quantified.
 
-  \<^descr> @{command "sublocale"}~\<open>name \<subseteq> expr \<WHERE>
-  eqns\<close>
+  \<^descr> @{command "sublocale"}~\<open>name \<subseteq> expr\<close>~@{keyword "rewrites"}~\<open>eqns\<close>
   interprets \<open>expr\<close> in the locale \<open>name\<close>.  A proof that
   the specification of \<open>name\<close> implies the specification of
   \<open>expr\<close> is required.  As in the localized version of the
@@ -826,10 +825,10 @@
     ;
     definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \<newline>
       @{syntax mixfix}? @'=' @{syntax term} + @'and');
-    equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
+    equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
   \<close>}
 
-  \<^descr> @{command "permanent_interpretation"}~\<open>expr \<DEFINING> defs \<WHERE> eqns\<close>
+  \<^descr> @{command "permanent_interpretation"}~\<open>expr \<DEFINING> defs\<close>~@{keyword "rewrites"}~\<open>eqns\<close>
   interprets \<open>expr\<close> in the current local theory.  The command
   generates proof obligations for the instantiated specifications.
   Instantiated declarations (in particular, facts) are added to the
diff -r 352c73a689da -r c3d6e570ccef src/Doc/Locales/Examples1.thy
--- a/src/Doc/Locales/Examples1.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Locales/Examples1.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -84,6 +84,6 @@
   In order to allow for the desired replacement, interpretation
   accepts \emph{equations} in addition to the parameter instantiation.
   These follow the locale expression and are indicated with the
-  keyword \isakeyword{where}.  This is the revised interpretation:
+  keyword \isakeyword{rewrites}.  This is the revised interpretation:
 \<close>
 end
diff -r 352c73a689da -r c3d6e570ccef src/Doc/Locales/Examples2.thy
--- a/src/Doc/Locales/Examples2.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Locales/Examples2.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -2,7 +2,7 @@
 imports Examples
 begin
   interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
-    where "int.less x y = (x < y)"
+    rewrites "int.less x y = (x < y)"
   proof -
     txt \<open>\normalsize The goals are now:
       @{subgoals [display]}
diff -r 352c73a689da -r c3d6e570ccef src/Doc/Locales/Examples3.thy
--- a/src/Doc/Locales/Examples3.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Doc/Locales/Examples3.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -17,7 +17,7 @@
   repeat the example from the previous section to illustrate this.\<close>
 
   interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
-    where "int.less x y = (x < y)"
+    rewrites "int.less x y = (x < y)"
   proof -
     show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
       by unfold_locales auto
@@ -47,7 +47,7 @@
   so they can be used in a later example.\<close>
 
   interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
-    where int_min_eq: "int.meet x y = min x y"
+    rewrites int_min_eq: "int.meet x y = min x y"
       and int_max_eq: "int.join x y = max x y"
   proof -
     show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
@@ -611,7 +611,7 @@
 
   \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
     \textit{prop} \\
-  \textit{equations} & ::= &  \textbf{where} \textit{equation} ( \textbf{and}
+  \textit{equations} & ::= &  \textbf{rewrites} \textit{equation} ( \textbf{and}
     \textit{equation} )$^*$  \\
   \textit{toplevel} & ::=
   & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
diff -r 352c73a689da -r c3d6e570ccef src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -504,7 +504,7 @@
 end
 
 interpretation x: logic_o "op \<and>" "Not"
-  where bool_logic_o: "x.lor_o(x, y) \<longleftrightarrow> x \<or> y"
+  rewrites bool_logic_o: "x.lor_o(x, y) \<longleftrightarrow> x \<or> y"
 proof -
   show bool_logic_o: "PROP logic_o(op \<and>, Not)" by unfold_locales fast+
   show "logic_o.lor_o(op \<and>, Not, x, y) \<longleftrightarrow> x \<or> y"
@@ -546,7 +546,7 @@
 lemmas less_thm = less_def
 end
 
-interpretation le: mixin gle where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+interpretation le: mixin gle rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin(gle)" by unfold_locales (rule grefl)
   note reflexive = this[unfolded mixin_def]
@@ -588,7 +588,7 @@
 locale mixin4_mixin = mixin4_base
 
 interpretation le: mixin4_mixin gle
-  where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+  rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
   note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
@@ -620,7 +620,7 @@
 locale mixin5_inherited = mixin5_base
 
 interpretation le5: mixin5_base gle
-  where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+  rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin5_base(gle)" by unfold_locales
   note reflexive = this[unfolded mixin5_base_def mixin_def]
@@ -648,7 +648,7 @@
 interpretation le6: mixin6_inherited gle
   by unfold_locales
 interpretation le6: mixin6_base gle
-  where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+  rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin6_base(gle)" by unfold_locales
   note reflexive = this[unfolded mixin6_base_def mixin_def]
@@ -669,7 +669,7 @@
 locale mixin7_inherited = reflexive
 
 interpretation le7: mixin7_base gle
-  where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+  rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin7_base(gle)" by unfold_locales
   note reflexive = this[unfolded mixin7_base_def mixin_def]
@@ -727,7 +727,7 @@
 end
 
 sublocale lgrp < "def"?: dgrp
-  where one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
+  rewrites one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
 proof -
   show "dgrp(prod)" by unfold_locales
   from this interpret d: dgrp .
@@ -766,7 +766,7 @@
 
 locale roundup = fixes x assumes true: "x \<longleftrightarrow> True"
 
-sublocale roundup \<subseteq> sub: roundup x where "x \<longleftrightarrow> True \<and> True"
+sublocale roundup \<subseteq> sub: roundup x rewrites "x \<longleftrightarrow> True \<and> True"
   apply unfold_locales apply (simp add: true) done
 lemma (in roundup) "True \<and> True \<longleftrightarrow> True" by (rule sub.true)
 
@@ -816,7 +816,7 @@
       and pnotnot: "\<And>x. pnot(pnot(x)) \<longleftrightarrow> x"
       and por_def: "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))"
     interpret loc: logic_o pand pnot
-      where por_eq: "\<And>x y. logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)"  (* FIXME *)
+      rewrites por_eq: "\<And>x y. logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)"  (* FIXME *)
     proof -
       show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
       fix x y
diff -r 352c73a689da -r c3d6e570ccef src/FOL/ex/Locale_Test/Locale_Test2.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test2.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test2.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -9,7 +9,7 @@
 begin
 
 interpretation le1: mixin_thy_merge gle gle'
-  where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
+  rewrites "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin_thy_merge(gle, gle')" by unfold_locales
   note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct1]
diff -r 352c73a689da -r c3d6e570ccef src/FOL/ex/Locale_Test/Locale_Test3.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test3.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test3.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -9,7 +9,7 @@
 begin
 
 interpretation le2: mixin_thy_merge gle gle'
-  where "reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)"
+  rewrites "reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)"
 proof -
   show "mixin_thy_merge(gle, gle')" by unfold_locales
   note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct2]
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -54,7 +54,7 @@
   with as few assumptions as possible.\<close>
 
 interpretation int: monoid \<Z>
-  where "carrier \<Z> = UNIV"
+  rewrites "carrier \<Z> = UNIV"
     and "mult \<Z> x y = x * y"
     and "one \<Z> = 1"
     and "pow \<Z> x n = x^n"
@@ -73,7 +73,7 @@
 qed
 
 interpretation int: comm_monoid \<Z>
-  where "finprod \<Z> f A = setprod f A"
+  rewrites "finprod \<Z> f A = setprod f A"
 proof -
   -- "Specification"
   show "comm_monoid \<Z>" by standard auto
@@ -88,7 +88,7 @@
 qed
 
 interpretation int: abelian_monoid \<Z>
-  where int_carrier_eq: "carrier \<Z> = UNIV"
+  rewrites int_carrier_eq: "carrier \<Z> = UNIV"
     and int_zero_eq: "zero \<Z> = 0"
     and int_add_eq: "add \<Z> x y = x + y"
     and int_finsum_eq: "finsum \<Z> f A = setsum f A"
@@ -114,7 +114,7 @@
      Since the morphisms through which the abelian structures are interpreted are
      not the identity, the equations of these interpretations are not inherited. *)
   (* FIXME *)
-  where "carrier \<Z> = UNIV"
+  rewrites "carrier \<Z> = UNIV"
     and "zero \<Z> = 0"
     and "add \<Z> x y = x + y"
     and "finsum \<Z> f A = setsum f A"
@@ -147,7 +147,7 @@
 qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
 
 interpretation int: "domain" \<Z>
-  where "carrier \<Z> = UNIV"
+  rewrites "carrier \<Z> = UNIV"
     and "zero \<Z> = 0"
     and "add \<Z> x y = x + y"
     and "finsum \<Z> f A = setsum f A"
@@ -173,7 +173,7 @@
 
 interpretation int (* FIXME [unfolded UNIV] *) :
   partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
-  where "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
+  rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
     and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
     and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
 proof -
@@ -189,7 +189,7 @@
 
 interpretation int (* FIXME [unfolded UNIV] *) :
   lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
-  where "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
+  rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y"
     and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y"
 proof -
   let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Algebra/Ring.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -95,7 +95,7 @@
 
 sublocale abelian_monoid <
   add!: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+  rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
     and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
     and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
   by (rule a_monoid) auto
@@ -113,7 +113,7 @@
 
 sublocale abelian_monoid <
   add!: comm_monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+  rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
     and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
     and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
     and "finprod \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = finsum G"
@@ -169,7 +169,7 @@
 
 sublocale abelian_group <
   add!: group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+  rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
     and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
     and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
     and "m_inv \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = a_inv G"
@@ -197,7 +197,7 @@
 
 sublocale abelian_group <
   add!: comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-  where "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
+  rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
     and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
     and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
     and "m_inv \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = a_inv G"
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -1197,7 +1197,7 @@
   "card = folding.F (\<lambda>_. Suc) 0"
 
 interpretation card!: folding "\<lambda>_. Suc" 0
-where
+rewrites
   "folding.F (\<lambda>_. Suc) 0 = card"
 proof -
   show "folding (\<lambda>_. Suc)" by standard rule
diff -r 352c73a689da -r c3d6e570ccef src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/GCD.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -1971,7 +1971,7 @@
 
 interpretation gcd_lcm_complete_lattice_nat:
   complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
-where "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
+rewrites "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
   and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
 proof -
   show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Groups_Big.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -472,7 +472,7 @@
   "setsum = comm_monoid_set.F plus 0"
 
 sublocale setsum!: comm_monoid_set plus 0
-where
+rewrites
   "comm_monoid_set.F plus 0 = setsum"
 proof -
   show "comm_monoid_set plus 0" ..
@@ -1063,7 +1063,7 @@
   "setprod = comm_monoid_set.F times 1"
 
 sublocale setprod!: comm_monoid_set times 1
-where
+rewrites
   "comm_monoid_set.F times 1 = setprod"
 proof -
   show "comm_monoid_set times 1" ..
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Groups_List.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -66,7 +66,7 @@
   "listsum  = monoid_list.F plus 0"
 
 sublocale listsum!: monoid_list plus 0
-where
+rewrites
  "monoid_list.F plus 0 = listsum"
 proof -
   show "monoid_list plus 0" ..
@@ -80,7 +80,7 @@
 begin
 
 sublocale listsum!: comm_monoid_list plus 0
-where
+rewrites
   "monoid_list.F plus 0 = listsum"
 proof -
   show "comm_monoid_list plus 0" ..
@@ -89,7 +89,7 @@
 qed
 
 sublocale setsum!: comm_monoid_list_set plus 0
-where
+rewrites
   "monoid_list.F plus 0 = listsum"
   and "comm_monoid_set.F plus 0 = setsum"
 proof -
@@ -333,7 +333,7 @@
   "listprod  = monoid_list.F times 1"
 
 sublocale listprod!: monoid_list times 1
-where
+rewrites
   "monoid_list.F times 1 = listprod"
 proof -
   show "monoid_list times 1" ..
@@ -347,7 +347,7 @@
 begin
 
 sublocale listprod!: comm_monoid_list times 1
-where
+rewrites
   "monoid_list.F times 1 = listprod"
 proof -
   show "comm_monoid_list times 1" ..
@@ -356,7 +356,7 @@
 qed
 
 sublocale setprod!: comm_monoid_list_set times 1
-where
+rewrites
   "monoid_list.F times 1 = listprod"
   and "comm_monoid_set.F times 1 = setprod"
 proof -
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -405,7 +405,7 @@
 qed
 
 interpretation heap!: partial_function_definitions Heap_ord Heap_lub
-  where "Heap_lub {} \<equiv> Heap Map.empty"
+  rewrites "Heap_lub {} \<equiv> Heap Map.empty"
 by (fact heap_interpretation)(simp add: Heap_lub_empty)
 
 lemma heap_step_admissible: 
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Lattices_Big.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -319,7 +319,7 @@
   "Inf_fin = semilattice_set.F inf"
 
 sublocale Inf_fin!: semilattice_order_set inf less_eq less
-where
+rewrites
   "semilattice_set.F inf = Inf_fin"
 proof -
   show "semilattice_order_set inf less_eq less" ..
@@ -337,7 +337,7 @@
   "Sup_fin = semilattice_set.F sup"
 
 sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
-where
+rewrites
   "semilattice_set.F sup = Sup_fin"
 proof -
   show "semilattice_order_set sup greater_eq greater" ..
@@ -492,7 +492,7 @@
 
 sublocale Min!: semilattice_order_set min less_eq less
   + Max!: semilattice_order_set max greater_eq greater
-where
+rewrites
   "semilattice_set.F min = Min"
   and "semilattice_set.F max = Max"
 proof -
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Library/Function_Growth.thy
--- a/src/HOL/Library/Function_Growth.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Library/Function_Growth.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -192,7 +192,7 @@
 text \<open>This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}.\<close>
 
 interpretation fun_order: preorder_equiv less_eq_fun less_fun
-  where "preorder_equiv.equiv less_eq_fun = equiv_fun"
+  rewrites "preorder_equiv.equiv less_eq_fun = equiv_fun"
 proof -
   interpret preorder: preorder_equiv less_eq_fun less_fun
   proof
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -1060,7 +1060,7 @@
   "mset_set = folding.F (\<lambda>x M. {#x#} + M) {#}"
 
 interpretation mset_set!: folding "\<lambda>x M. {#x#} + M" "{#}"
-where
+rewrites
   "folding.F (\<lambda>x M. {#x#} + M) {#} = mset_set"
 proof -
   interpret comp_fun_commute "\<lambda>x M. {#x#} + M"
@@ -1223,7 +1223,7 @@
   where "msetsum = comm_monoid_mset.F plus 0"
 
 sublocale msetsum!: comm_monoid_mset plus 0
-  where "comm_monoid_mset.F plus 0 = msetsum"
+  rewrites "comm_monoid_mset.F plus 0 = msetsum"
 proof -
   show "comm_monoid_mset plus 0" ..
   from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" ..
@@ -1281,7 +1281,7 @@
   where "msetprod = comm_monoid_mset.F times 1"
 
 sublocale msetprod!: comm_monoid_mset times 1
-  where "comm_monoid_mset.F times 1 = msetprod"
+  rewrites "comm_monoid_mset.F times 1 = msetprod"
 proof -
   show "comm_monoid_mset times 1" ..
   show "comm_monoid_mset.F times 1 = msetprod" using msetprod_def ..
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Library/Saturated.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -215,7 +215,7 @@
 end
 
 interpretation Inf_sat!: semilattice_neutr_set min "top :: 'a::len sat"
-where
+rewrites
   "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
 proof -
   show "semilattice_neutr_set min (top :: 'a sat)"
@@ -225,7 +225,7 @@
 qed
 
 interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
-where
+rewrites
   "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
 proof -
   show "semilattice_neutr_set max (bot :: 'a sat)"
diff -r 352c73a689da -r c3d6e570ccef src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/List.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -5151,7 +5151,7 @@
   "sorted_list_of_set = folding.F insort []"
 
 sublocale sorted_list_of_set!: folding insort Nil
-where
+rewrites
   "folding.F insort [] = sorted_list_of_set"
 proof -
   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
diff -r 352c73a689da -r c3d6e570ccef src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/Partial_Function.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -283,12 +283,12 @@
 
 interpretation tailrec!:
   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
-  where "flat_lub undefined {} \<equiv> undefined"
+  rewrites "flat_lub undefined {} \<equiv> undefined"
 by (rule flat_interpretation)(simp add: flat_lub_def)
 
 interpretation option!:
   partial_function_definitions "flat_ord None" "flat_lub None"
-  where "flat_lub None {} \<equiv> None"
+  rewrites "flat_lub None {} \<equiv> None"
 by (rule flat_interpretation)(simp add: flat_lub_def)
 
 
diff -r 352c73a689da -r c3d6e570ccef src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -469,7 +469,7 @@
 subsubsection \<open>Total order @{text "<="} on @{typ int}\<close>
 
 interpretation int: dpo "op <= :: [int, int] => bool"
-  where "(dpo.less (op <=) (x::int) y) = (x < y)"
+  rewrites "(dpo.less (op <=) (x::int) y) = (x < y)"
   txt \<open>We give interpretation for less, but not @{text is_inf} and @{text is_sub}.\<close>
 proof -
   show "dpo (op <= :: [int, int] => bool)"
@@ -488,7 +488,7 @@
   apply (rule int.abs_test) done
 
 interpretation int: dlat "op <= :: [int, int] => bool"
-  where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
+  rewrites meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
     and join_eq: "dlat.join (op <=) (x::int) y = max x y"
 proof -
   show "dlat (op <= :: [int, int] => bool)"
@@ -525,7 +525,7 @@
 subsubsection \<open>Total order @{text "<="} on @{typ nat}\<close>
 
 interpretation nat: dpo "op <= :: [nat, nat] => bool"
-  where "dpo.less (op <=) (x::nat) y = (x < y)"
+  rewrites "dpo.less (op <=) (x::nat) y = (x < y)"
   txt \<open>We give interpretation for less, but not @{text is_inf} and @{text is_sub}.\<close>
 proof -
   show "dpo (op <= :: [nat, nat] => bool)"
@@ -539,7 +539,7 @@
 qed
 
 interpretation nat: dlat "op <= :: [nat, nat] => bool"
-  where "dlat.meet (op <=) (x::nat) y = min x y"
+  rewrites "dlat.meet (op <=) (x::nat) y = min x y"
     and "dlat.join (op <=) (x::nat) y = max x y"
 proof -
   show "dlat (op <= :: [nat, nat] => bool)"
@@ -576,7 +576,7 @@
 subsubsection \<open>Lattice @{text "dvd"} on @{typ nat}\<close>
 
 interpretation nat_dvd: dpo "op dvd :: [nat, nat] => bool"
-  where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
+  rewrites "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
   txt \<open>We give interpretation for less, but not @{text is_inf} and @{text is_sub}.\<close>
 proof -
   show "dpo (op dvd :: [nat, nat] => bool)"
@@ -590,7 +590,7 @@
 qed
 
 interpretation nat_dvd: dlat "op dvd :: [nat, nat] => bool"
-  where "dlat.meet (op dvd) (x::nat) y = gcd x y"
+  rewrites "dlat.meet (op dvd) (x::nat) y = gcd x y"
     and "dlat.join (op dvd) (x::nat) y = lcm x y"
 proof -
   show "dlat (op dvd :: [nat, nat] => bool)"
@@ -835,7 +835,7 @@
 subsubsection \<open>Interpretation of Functions\<close>
 
 interpretation Dfun: Dmonoid "op o" "id :: 'a => 'a"
-  where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
+  rewrites "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
 (*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
 proof -
   show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc)
@@ -885,7 +885,7 @@
   by rule simp
 
 interpretation Dfun: Dgrp "op o" "id :: unit => unit"
-  where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
+  rewrites "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
 proof -
   have "Dmonoid op o (id :: 'a => 'a)" ..
   note Dmonoid = this
diff -r 352c73a689da -r c3d6e570ccef src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 04 08:13:52 2015 +0100
@@ -405,7 +405,7 @@
 val interpretation_args =
   Parse.!!! (Parse_Spec.locale_expression true) --
     Scan.optional
-      (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
+      (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
 
 val _ =
   Outer_Syntax.command @{command_keyword sublocale}
diff -r 352c73a689da -r c3d6e570ccef src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Nov 04 08:13:49 2015 +0100
+++ b/src/Pure/Pure.thy	Wed Nov 04 08:13:52 2015 +0100
@@ -11,8 +11,8 @@
     "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
     "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
     "infixl" "infixr" "is" "notes" "obtains" "open" "output"
-    "overloaded" "pervasive" "premises" "private" "qualified" "shows"
-    "structure" "unchecked" "where" "when" "|"
+    "overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
+    "shows" "structure" "unchecked" "where" "when" "|"
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl == ""