# HG changeset patch
# User wenzelm
# Date 1375882533 -7200
# Node ID 73e32ed924b3eeec85966e00deeb8aaad0593d92
# Parent  a806aa7a5370960c37d553bb2ce055ff72d41030
more NEWS and CONTRIBUTORS;

diff -r a806aa7a5370 -r 73e32ed924b3 CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Aug 02 15:42:47 2013 +0900
+++ b/CONTRIBUTORS	Wed Aug 07 15:35:33 2013 +0200
@@ -6,6 +6,10 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* Summer 2013: Christian Sternagel, JAIST
+  Improved support for adhoc overloading of constants, including
+  documentation and examples.
+
 * May 2013: Florian Haftmann, TUM
   Ephemeral interpretation in local theories.
 
diff -r a806aa7a5370 -r 73e32ed924b3 NEWS
--- a/NEWS	Fri Aug 02 15:42:47 2013 +0900
+++ b/NEWS	Wed Aug 07 15:35:33 2013 +0200
@@ -106,6 +106,9 @@
 
 *** HOL ***
 
+* Improved support for adhoc overloading of constants (see also
+isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).
+
 * Attibute 'code': 'code' now declares concrete and abstract code equations uniformly.
 Use explicit 'code equation' and 'code abstract' to distinguish both when desired.
 
diff -r a806aa7a5370 -r 73e32ed924b3 src/Doc/IsarRef/document/root.tex
--- a/src/Doc/IsarRef/document/root.tex	Fri Aug 02 15:42:47 2013 +0900
+++ b/src/Doc/IsarRef/document/root.tex	Wed Aug 07 15:35:33 2013 +0200
@@ -40,7 +40,8 @@
   Lars Noschinski, \\
   David von Oheimb,
   Larry Paulson,
-  Sebastian Skalberg
+  Sebastian Skalberg, \\
+  Christian Sternagel
 }
 
 \makeindex