:- : ind -> bool -> boolAC : bool -> bool -> boolAbbrev : bool -> boolCase : α -> boolCong : bool -> boolExclude : α -> boolExcludeFrag : α -> boolFRAG : α -> boolIfCases : boolIgnAsm : α -> boolNoAsms : boolReq0 : boolReqD : boolhide : bool -> bool -> boolresconj : bool -> bool -> boolstmarker : α -> αsuspendimp : bool -> bool -> boolsuspendlabel : ind -> bool -> boolunint : α -> αusing : ind -> boolusingThm : bool -> boolAC_DEF⊢ ∀b1 b2. marker$AC b1 b2 ⇔ b1 ∧ b2
Abbrev_def⊢ ∀x. Abbrev x ⇔ x
Case_def⊢ ∀X. Case X ⇔ T
Cong_def⊢ ∀x. Cong x ⇔ x
ExcludeFrag_def⊢ ∀x. ExcludeFrag x ⇔ T
Exclude_def⊢ ∀x. Exclude x ⇔ T
FRAG_def⊢ ∀x. FRAG x ⇔ T
IfCases_def⊢ IfCases ⇔ T
IgnAsm_def⊢ ∀v. IgnAsm v ⇔ T
NoAsms⊢ NoAsms ⇔ T
Req0_def⊢ marker$Req0 ⇔ T
ReqD_def⊢ marker$ReqD ⇔ T
hide_def⊢ ∀nm x. marker$hide nm x ⇔ x
label_def⊢ ∀lab argument. (lab :- argument) ⇔ argument
resconj_def⊢ resconj = $/\
stmarker_def⊢ ∀x. stmarker x = x
suspendimp_def⊢ suspendimp = $==>
suspendlabel_def⊢ ∀l arg. suspendlabel l arg ⇔ arg
unint_def⊢ ∀x. unint x = x
usingThm_def⊢ ∀b. marker$usingThm b ⇔ b
using_def⊢ ∀x. marker$using x ⇔ T
Abbrev_CONG⊢ r1 = r2 ⇒ (Abbrev (v = r1) ⇔ Abbrev (v = r2))
add_Case⊢ ∀X. P ⇔ Case X ⇒ P
elim_Case⊢ (Case X ∧ Y ⇔ Y) ∧ (Y ∧ Case X ⇔ Y) ∧ (Case X ⇒ Y ⇔ Y)
hideCONG⊢ marker$hide nm x ⇔ marker$hide nm x
move_left_conj⊢ ∀p q m.
(p ∧ stmarker m ⇔ stmarker m ∧ p) ∧
((stmarker m ∧ p) ∧ q ⇔ stmarker m ∧ p ∧ q) ∧
(p ∧ stmarker m ∧ q ⇔ stmarker m ∧ p ∧ q)
move_left_disj⊢ ∀p q m.
(p ∨ stmarker m ⇔ stmarker m ∨ p) ∧
((stmarker m ∨ p) ∨ q ⇔ stmarker m ∨ p ∨ q) ∧
(p ∨ stmarker m ∨ q ⇔ stmarker m ∨ p ∨ q)
move_right_conj⊢ ∀p q m.
(stmarker m ∧ p ⇔ p ∧ stmarker m) ∧
(p ∧ q ∧ stmarker m ⇔ (p ∧ q) ∧ stmarker m) ∧
((p ∧ stmarker m) ∧ q ⇔ (p ∧ q) ∧ stmarker m)
move_right_disj⊢ ∀p q m.
(stmarker m ∨ p ⇔ p ∨ stmarker m) ∧
(p ∨ q ∨ stmarker m ⇔ (p ∨ q) ∨ stmarker m) ∧
((p ∨ stmarker m) ∨ q ⇔ (p ∨ q) ∨ stmarker m)