--- a/src/HOL/Hilbert_Choice.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Hilbert_Choice.thy Mon Sep 23 13:32:38 2024 +0200
@@ -17,11 +17,11 @@
where someI: "P x \<Longrightarrow> P (Eps P)"
syntax (epsilon)
- "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3\<some>_./ _)" [0, 10] 10)
+ "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3\<some>_./ _)\<close> [0, 10] 10)
syntax (input)
- "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3@ _./ _)" [0, 10] 10)
+ "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3@ _./ _)\<close> [0, 10] 10)
syntax
- "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3SOME _./ _)" [0, 10] 10)
+ "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3SOME _./ _)\<close> [0, 10] 10)
syntax_consts "_Eps" \<rightleftharpoons> Eps