axioms : unit -> thm list

SYNOPSIS

Returns the current set of axioms.

DESCRIPTION

A call axioms() returns the current list of axioms.

FAILURE CONDITIONS

Never fails.

EXAMPLE

Under normal circumstances, the list of axioms will be as follows, containing the axioms of infinity, choice and extensionality.

  # axioms();;
  val it : thm list =
    [|- ?f. ONE_ONE f /\ ~ONTO f; |- !P x. P x ==> P ((@) P);
     |- !t. (\x. t x) = t]

If other axioms are used, the consistency of the resulting theory cannot be guaranteed. However, new definitions and type definitions are always safe and are not considered as true `axioms'.