# HG changeset patch
# User ballarin
# Date 1448143332 -3600
# Node ID 4653d0835e6ec3dbea7b64e6ae638088f9434ea2
# Parent  cb142691ef442ed83966f74d172b3730a246ec1b
Updates to the revision history of the locales tutorial.

diff -r cb142691ef44 -r 4653d0835e6e src/Doc/Locales/Examples3.thy
--- a/src/Doc/Locales/Examples3.thy	Sat Nov 21 23:02:07 2015 +0100
+++ b/src/Doc/Locales/Examples3.thy	Sat Nov 21 23:02:12 2015 +0100
@@ -631,14 +631,15 @@
 \end{table}
 \<close>
 
-text \<open>\textbf{Revision History.}  For the present third revision of
-  the tutorial, much of the explanatory text
-  was rewritten.  Inheritance of interpretation equations is
-  available with the forthcoming release of Isabelle, which at the
-  time of editing these notes is expected for the end of 2009.
+text \<open>\textbf{Revision History.}  The present fourth revision of the
+  tutorial accommodates minor updates to the syntax of the locale commands
+  and the handling of notation under morphisms introduced with Isabelle 2016.
+  For the third revision of the tutorial, which corresponds to the published
+  version, much of the explanatory text was rewritten.  Inheritance of
+  interpretation equations was made available with Isabelle 2009-1.
   The second revision accommodates changes introduced by the locales
   reimplementation for Isabelle 2009.  Most notably locale expressions
-  have been generalised from renaming to instantiation.\<close>
+  were generalised from renaming to instantiation.\<close>
 
 text \<open>\textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
   Randy Pollack, Andreas Schropp, Christian Sternagel and Makarius Wenzel