If M is a term of type bool, a call new_axiom(name,M) creates
a theorem
|- tm
and stores it away in the current theory segment under name.
FAILURE
Fails if the given term does not have type bool.
EXAMPLE
- new_axiom("untrue", Term `!x. x = 1`);
> val it = |- !x. x = 1 : thm
COMMENTS
For most purposes, it is unnecessary to declare new axioms: all
of classical mathematics can be derived by definitional extension
alone. Proceeding by definition is not only more elegant, but also
guarantees the consistency of the deductions made. However, there are
certain entities which cannot be modelled in simple type theory without
further axioms, such as higher transfinite ordinals.