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]}