new_basic_definition : term -> thm
# let googolplex = new_basic_definition `googolplex = 10 EXP (10 EXP 100)`;; val googolplex : thm = |- googolplex = 10 EXP (10 EXP 100)
# let true_def = new_basic_definition `true <=> T`;; val true_def : thm = |- true <=> T
# new_basic_definition `trivial <=> !x y:A. x = y`;; Exception: Failure "new_definition: Type variables not reflected in constant".