Theory Generic_Context

theory Generic_Context
  imports Context_Notation
begin

locale "context" =
  context_notation +
  assumes
    compose_context_iff [simp]: "⋀(c :: 'c) c' (t :: 't). (c ∘⇩c c')⟨t⟩ = c⟨c'⟨t⟩⟩" and
    apply_hole [simp]: "⋀t. □⟨t⟩ = t" and
    apply_context_eq: "⋀c t t'. c⟨t⟩ = c⟨t'⟩ ⟹ t = t'"

end