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_syntax
begin
notation PNT_const_C⇩1 (‹C⇩1›)
notation norm (‹∥_∥›)
notation Suc (‹_⇩+› [101] 100)
end

end