Theory Term_Order_Notation

theory Term_Order_Notation
  imports Main
begin

locale term_order_notation =
  fixes less⇩t :: "'t ⇒ 't ⇒ bool"
begin

notation less⇩t (infix "≺⇩t" 50)

abbreviation "less_eq⇩t ≡ (≺⇩t)⇧=⇧="

notation less_eq⇩t (infix "≼⇩t" 50)

end

end