--- a/src/HOL/Induct/SList.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Induct/SList.thy Fri Sep 20 19:51:08 2024 +0200
@@ -84,15 +84,15 @@
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
no_notation
- Nil ("[]") and
- Cons (infixr "#" 65)
+ Nil (\<open>[]\<close>) and
+ Cons (infixr \<open>#\<close> 65)
definition
- Nil :: "'a list" ("[]") where
+ Nil :: "'a list" (\<open>[]\<close>) where
"Nil = Abs_List(NIL)"
definition
- "Cons" :: "['a, 'a list] => 'a list" (infixr "#" 65) where
+ "Cons" :: "['a, 'a list] => 'a list" (infixr \<open>#\<close> 65) where
"x#xs = Abs_List(CONS (Leaf x)(Rep_List xs))"
definition