--- a/src/Doc/Tutorial/ToyList/ToyList.thy Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy Fri Sep 27 23:47:45 2024 +0200
@@ -9,12 +9,12 @@
the concrete syntax and name space of theory \<^theory>\<open>Main\<close> as follows.
\<close>
-no_notation Nil (\<open>[]\<close>) and Cons (infixr \<open>#\<close> 65) and append (infixr \<open>@\<close> 65)
+no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
hide_type list
hide_const rev
-datatype 'a list = Nil (\<open>[]\<close>)
- | Cons 'a "'a list" (infixr \<open>#\<close> 65)
+datatype 'a list = Nil ("[]")
+ | Cons 'a "'a list" (infixr "#" 65)
text\<open>\noindent
The datatype\index{datatype@\isacommand {datatype} (command)}
@@ -47,7 +47,7 @@
in this order, because Isabelle insists on definition before use:
\<close>
-primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr \<open>@\<close> 65) where
+primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"