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 galois_rel.Galois (‹'((⇘_⇙)⪅(⇘(_) (_)⇙)')›)
  notation Galois_infix (‹(_) (⇘_⇙)⪅(⇘(_) (_)⇙) (_)› [51,51,51,51,51] 50)
  notation ge_Galois (‹'((⇘(_) (_)⇙)⪆(⇘_⇙)')›)
  notation ge_Galois_infix (‹(_) (⇘(_) (_)⇙)⪆(⇘_⇙) (_)› [51,51,51,51,51] 50)
end

end