Definition. Building up HOL › Disjunction [isa-0004]
\dfrac {A}{A \lor B}\text {\small disjI1}\quad
\dfrac {B}{A \lor B}\text {\small disjI2}\quad
\dfrac {\begin {array}{lcc}&A & B\\ & \vdots & \vdots \\A \lor B & C & C\end {array}}{C}\text {\small disjE}
axiomatization
disj :: "bool ⇒ bool ⇒ bool" (infixr "∨" 30)
where
disjI1 : "A ⟹ (A ∨ B)" and
disjI2 : "B ⟹ (A ∨ B)" and
disjE : "⟦ A ∨ B ; A ⟹ C ; B ⟹ C ⟧ ⟹ C"