src/Doc/Tutorial/Recdef/examples.thy
changeset 69505 cc2d676d5395
parent 67406 23307fd33906
--- a/src/Doc/Tutorial/Recdef/examples.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/Recdef/examples.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -36,7 +36,7 @@
 text\<open>\noindent
 This time the measure is the length of the list, which decreases with the
 recursive call; the first component of the argument tuple is irrelevant.
-The details of tupled $\lambda$-abstractions @{text"\<lambda>(x\<^sub>1,\<dots>,x\<^sub>n)"} are
+The details of tupled $\lambda$-abstractions \<open>\<lambda>(x\<^sub>1,\<dots>,x\<^sub>n)\<close> are
 explained in \S\ref{sec:products}, but for now your intuition is all you need.
 
 Pattern matching\index{pattern matching!and \isacommand{recdef}}