Theory Entailment

theory Entailment
imports Main "HOL-Library.FSet"
begin

type_synonym 'form entailment = "('form fset × 'form)"

abbreviation entails :: "'form fset ⇒ 'form ⇒ 'form entailment" (infix ‹⊢› 50)
  where "a ⊢ c ≡ (a, c)"

fun add_ctxt :: "'form fset ⇒ 'form entailment ⇒ 'form entailment" where
  "add_ctxt Δ (Γ ⊢ c) = (Γ |∪| Δ ⊢ c)"

end