new_axiom : term -> thm

Sets up a new axiom.

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

Fails if the given term does not have type bool.

  # 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.

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.

axioms, mk_thm, new_definition.