theorems : (string * thm) list ref
# theorems;;
val it : (string * thm) list ref =
contents =
[("ABSORPTION", |- !x s. x IN s <=> x INSERT s = s);
("ABS_SIMP", |- !t1 t2. (\x. t1) t2 = t1);
("ADD", |- (!n. 0 + n = n) /\ (!m n. SUC m + n = SUC (m + n)));
("ADD1", |- !m. SUC m = m + 1); ("ADD_0", |- !m. m + 0 = m);
...