# HG changeset patch
# User nipkow
# Date 1447323746 -3600
# Node ID b1c24adc15814973c1c05ef16a629bc088b7fe5f
# Parent  712d3d64c38b55e6995de5dd73e5de00a690de56
tuned

diff -r 712d3d64c38b -r b1c24adc1581 src/Doc/Prog_Prove/Basics.thy
--- a/src/Doc/Prog_Prove/Basics.thy	Thu Nov 12 11:05:38 2015 +0100
+++ b/src/Doc/Prog_Prove/Basics.thy	Thu Nov 12 11:22:26 2015 +0100
@@ -29,7 +29,7 @@
 \item[type variables,]
   denoted by @{typ 'a}, @{typ 'b}, etc., like in ML\@.
 \end{description}
-Note that @{typ"'a \<Rightarrow> 'b list"} means @{typ[source]"'a \<Rightarrow> ('b list)"},
+Note that @{typ"'a \<Rightarrow> 'b list"} means \noquotes{@{typ[source]"'a \<Rightarrow> ('b list)"}},
 not @{typ"('a \<Rightarrow> 'b) list"}: postfix type constructors have precedence
 over @{text"\<Rightarrow>"}.