Theory First_Order_Clause.Context_Notation

theory Context_Notation
  imports Main
begin

locale apply_context_notation = 
  fixes apply_context :: "'c ⇒ 't ⇒ 't"
begin

notation apply_context (‹_⟨_⟩› [1000, 0] 1000)

end

locale hole_notation = 
  fixes hole :: "'c"
begin

notation hole (‹□›)

end

locale compose_context_notation =
  fixes compose_context :: "'c ⇒ 'c ⇒ 'c"
begin

notation compose_context (infixl ‹∘⇩c› 75)

end

locale context_notation = 
  apply_context_notation + 
  hole_notation +
  compose_context_notation

end