Theory Galois_Relator_Syntax

✐‹creator "Kevin Kappelmann"›
section ‹Syntax Bundles for Galois Relator›
theory Galois_Relator_Syntax
  imports
    Galois_Relator_Base
begin

abbreviation "Galois_infix x L R r y ≡ galois_rel.Galois L R r x y"
abbreviation (input) "ge_Galois R r L ≡ galois_rel.ge_Galois_left L R r"
abbreviation (input) "ge_Galois_infix y R r L x ≡ ge_Galois R r L y x"

bundle galois_rel_Galois_syntax
begin
  notation (input) galois_rel.Galois (‹'((⇘_⇙)⪅(⇘(_) (_)⇙)')›)
  notation (output) galois_rel.Galois (‹'((⇘_⇙)⪅(⇘('(_')) ('(_'))⇙)')›)
  notation (input) Galois_infix (‹_ (⇘_⇙)⪅(⇘(_) (_)⇙) _› [51,0,0,51] 50)
  notation (output) Galois_infix (‹_ (⇘_⇙)⪅(⇘('(_')) ('(_'))⇙) _› [51,0,0,51] 50)
  notation (input) ge_Galois (‹'((⇘(_) (_)⇙)⪆(⇘_⇙)')›)
  notation (output) ge_Galois (‹'((⇘('(_')) ('(_'))⇙)⪆(⇘_⇙)')›)
  notation (input) ge_Galois_infix (‹_ (⇘(_) (_)⇙)⪆(⇘_⇙) _›  [51,0,0,51] 50)
  notation (output) ge_Galois_infix (‹_ (⇘('(_')) ('(_'))⇙)⪆(⇘_⇙) _›  [51,0,0,51] 50)
end

end