--- a/src/HOL/Archimedean_Field.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Archimedean_Field.thy Mon Sep 23 13:32:38 2024 +0200
@@ -205,7 +205,7 @@
subsection \<open>Floor function\<close>
class floor_ceiling = archimedean_field +
- fixes floor :: "'a \<Rightarrow> int" ("\<lfloor>_\<rfloor>")
+ fixes floor :: "'a \<Rightarrow> int" (\<open>\<lfloor>_\<rfloor>\<close>)
assumes floor_correct: "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
lemma floor_unique: "of_int z \<le> x \<Longrightarrow> x < of_int z + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = z"
@@ -427,7 +427,7 @@
subsection \<open>Ceiling function\<close>
-definition ceiling :: "'a::floor_ceiling \<Rightarrow> int" ("\<lceil>_\<rceil>")
+definition ceiling :: "'a::floor_ceiling \<Rightarrow> int" (\<open>\<lceil>_\<rceil>\<close>)
where "\<lceil>x\<rceil> = - \<lfloor>- x\<rfloor>"
lemma ceiling_correct: "of_int \<lceil>x\<rceil> - 1 < x \<and> x \<le> of_int \<lceil>x\<rceil>"