Theory HOL_Syntax_Bundles_Orders

✐‹creator "Kevin Kappelmann"›
section ‹Order Syntax›
theory HOL_Syntax_Bundles_Orders
  imports HOL.Orderings
begin

bundle HOL_order_syntax
begin
notation
  less_eq  (‹'(≤')›) and
  less_eq  (‹(‹notation=‹infix ≤››_/ ≤ _)›  [51, 51] 50) and
  less  (‹'(<')›) and
  less  (‹(‹notation=‹infix <››_/ < _)›  [51, 51] 50)
notation (input) greater_eq (infix ‹≥› 50)
notation (input) greater (infix ‹>› 50)
notation (ASCII)
  less_eq  (‹'(<=')›) and
  less_eq  (‹(‹notation=‹infix <=››_/ <= _)› [51, 51] 50)
notation (input) greater_eq (infix ‹>=› 50)
end

end