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