AC : thm -> term -> thm
acth = |- m _ n = n _ m /\ (m _ n) _ p = m _ n _ p /\ m _ n _ p = n _ m _ p
|- (p _ q = q _ p) /\ ((p _ q) _ r = p _ q _ r) /\ (p _ q _ r = q _ p _ r) /\ (p _ p = p) /\ (p _ p _ q = p _ q)
# AC ADD_AC `1 + 2 + 3 = 2 + 1 + 3`;; val it : thm = |- 1 + 2 + 3 = 2 + 1 + 3 # AC CONJ_ACI `p /\ (q /\ p) <=> (p /\ q) /\ (p /\ q)`;; val it : thm = |- p /\ q /\ p <=> (p /\ q) /\ p /\ q