# HG changeset patch
# User wenzelm
# Date 1436172974 -7200
# Node ID 98b64a1deff098665108f77907f31ada42ea51c0
# Parent  ca1e07005b8b67ea0a42b2996b9a3ec156c3a546
tuned;

diff -r ca1e07005b8b -r 98b64a1deff0 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 10:54:15 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 10:56:14 2015 +0200
@@ -58,9 +58,7 @@
   nicely, but they also mean that HOL requires some sophistication
   from the user.  In particular, an understanding of Hindley-Milner
   type-inference with type-classes, which are both used extensively in
-  the standard libraries and applications.  Beginners can set
-  @{attribute show_types} or even @{attribute show_sorts} to get more
-  explicit information about the result of type-inference.\<close>
+  the standard libraries and applications.\<close>
 
 
 chapter \<open>Derived specification elements\<close>