--- a/src/HOL/Library/OptionalSugar.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Fri Sep 20 19:51:08 2024 +0200
@@ -27,7 +27,7 @@
(* append *)
syntax (latex output)
- "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^latex>\<open>\\isacharat\<close>" 65)
+ "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl \<open>\<^latex>\<open>\isacharat\<close>\<close> 65)
translations
"_appendL xs ys" <= "xs @ ys"
"_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
@@ -36,8 +36,8 @@
(* deprecated, use thm with style instead, will be removed *)
(* aligning equations *)
notation (tab output)
- "HOL.eq" ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>=\<^latex>\<open>}\\putisatab\\isa{\<close> (_)" [50,49] 50) and
- "Pure.eq" ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>\<equiv>\<^latex>\<open>}\\putisatab\\isa{\<close> (_)")
+ "HOL.eq" (\<open>(_) \<^latex>\<open>}\putisatab\isa{\ \<close>=\<^latex>\<open>}\putisatab\isa{\<close> (_)\<close> [50,49] 50) and
+ "Pure.eq" (\<open>(_) \<^latex>\<open>}\putisatab\isa{\ \<close>\<equiv>\<^latex>\<open>}\putisatab\isa{\<close> (_)\<close>)
(* Let *)
translations
@@ -53,21 +53,21 @@
(* type constraints with spacing *)
no_syntax (output)
- "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3)
- "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3)
+ "_constrain" :: "logic => type => logic" (\<open>_::_\<close> [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" (\<open>_::_\<close> [4, 0] 3)
syntax (output)
- "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
- "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3)
+ "_constrain" :: "logic => type => logic" (\<open>_ :: _\<close> [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" (\<open>_ :: _\<close> [4, 0] 3)
(* sorts as intersections *)
syntax (output)
- "_topsort" :: "sort" ("\<top>" 1000)
- "_sort" :: "classes => sort" ("'(_')" 1000)
- "_classes" :: "id => classes => classes" ("_ \<inter> _" 1000)
- "_classes" :: "longid => classes => classes" ("_ \<inter> _" 1000)
+ "_topsort" :: "sort" (\<open>\<top>\<close> 1000)
+ "_sort" :: "classes => sort" (\<open>'(_')\<close> 1000)
+ "_classes" :: "id => classes => classes" (\<open>_ \<inter> _\<close> 1000)
+ "_classes" :: "longid => classes => classes" (\<open>_ \<inter> _\<close> 1000)
end
(*>*)