--- a/src/HOL/Power.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Power.thy Mon Sep 23 13:32:38 2024 +0200
@@ -14,16 +14,16 @@
class power = one + times
begin
-primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80)
+primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr \<open>^\<close> 80)
where
power_0: "a ^ 0 = 1"
| power_Suc: "a ^ Suc n = a * a ^ n"
notation (latex output)
- power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+ power (\<open>(_\<^bsup>_\<^esup>)\<close> [1000] 1000)
text \<open>Special syntax for squares.\<close>
-abbreviation power2 :: "'a \<Rightarrow> 'a" ("(_\<^sup>2)" [1000] 999)
+abbreviation power2 :: "'a \<Rightarrow> 'a" (\<open>(_\<^sup>2)\<close> [1000] 999)
where "x\<^sup>2 \<equiv> x ^ 2"
end