--- 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} ( ``$<$'' $|$