| changeset 81128 | 5b201b24d99b |
| parent 80983 | 2cc651d3ce8e |
| child 81136 | 2b949a3bfaac |
--- a/src/Doc/Tutorial/ToyList/ToyList.thy Tue Oct 08 15:02:17 2024 +0200 +++ b/src/Doc/Tutorial/ToyList/ToyList.thy Tue Oct 08 15:44:11 2024 +0200 @@ -9,7 +9,7 @@ the concrete syntax and name space of theory \<^theory>\<open>Main\<close> as follows. \<close> -no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65) +no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65) hide_type list hide_const rev