--- a/src/ZF/List.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/List.thy Thu Jan 03 21:15:52 2019 +0100
@@ -15,8 +15,8 @@
syntax
- "_Nil" :: i ("[]")
- "_List" :: "is => i" ("[(_)]")
+ "_Nil" :: i (\<open>[]\<close>)
+ "_List" :: "is => i" (\<open>[(_)]\<close>)
translations
"[x, xs]" == "CONST Cons(x, [xs])"
@@ -45,7 +45,7 @@
consts
map :: "[i=>i, i] => i"
set_of_list :: "i=>i"
- app :: "[i,i]=>i" (infixr "@" 60)
+ app :: "[i,i]=>i" (infixr \<open>@\<close> 60)
(*map is a binding operator -- it applies to meta-level functions, not
object-level functions. This simplifies the final form of term_rec_conv,