new_axiom : string * term -> thm
STRUCTURE
SYNOPSIS
Install a new axiom in the current theory.
DESCRIPTION
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.
SEEALSO
HOL  Kananaskis-13