new_axiom : term -> thm

SYNOPSIS
Sets up a new axiom.

DESCRIPTION
If tm is a term of type bool, a call new_axiom tm creates a theorem
   |- tm

FAILURE CONDITIONS
Fails if the given term does not have type bool.

EXAMPLE
  # let ax = new_axiom `x = 1`;;
  val ax : thm = |- x = 1
Note that as with all theorems, variables are implicitly universally quantified, so this axiom asserts that all numbers are equal to 1. Of course, we can then derive a contradiction:
  CONV_RULE NUM_REDUCE_CONV (INST [`0`,`x:num`] ax);;
  val it : thm = |- F
Normal use of HOL Light should avoid asserting axioms. They can lead to inconsistency, albeit not in such an obvious way. Provided theories are extended by definitions, consistency is preserved.

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.

SEE ALSO
axioms, mk_thm, new_definition.