the_definitions : thm list ref
# !the_definitions;; val it : thm list = [|- !(<<) p s t. superadmissible (<<) p s t <=> admissible (<<) (\f a. T) s p ==> tailadmissible (<<) p s t; ... ... |- (/\) = (\p q. (\f. f p q) = (\f. f T T)); |- T <=> (\p. p) = (\p. p)]
# new_definition `false <=> F`;; val it : thm = |- false <=> F
# !the_definitions;; val it : thm list = [|- false <=> F; ... ... |- (/\) = (\p q. (\f. f p q) = (\f. f T T)); |- T <=> (\p. p) = (\p. p)]