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: \ end