Updates to the revision history of the locales tutorial.
authorballarin
Sat, 21 Nov 2015 23:02:12 +0100
changeset 61732 4653d0835e6e
parent 61731 cb142691ef44
child 61733 00fcff12c59f
Updates to the revision history of the locales tutorial.
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