Theory PNT_Notation

theory PNT_Notation
imports
  "Prime_Number_Theorem.Prime_Counting_Functions"
begin

definition "PNT_const_C⇩1 ≡ 1 / 952320 :: real"

abbreviation nat_powr
  (infixr "nat'_powr" 80)
where
  "n nat_powr x ≡ (of_nat n) powr x"

bundle pnt_notation
begin
notation PNT_const_C⇩1 ("C⇩1")
notation norm ("∥_∥")
notation Suc ("_⇩+" [101] 100)
end

bundle no_pnt_notation
begin
no_notation PNT_const_C⇩1 ("C⇩1")
no_notation norm ("∥_∥")
no_notation Suc ("_⇩+" [101] 100)
end

end