axioms : unit -> thm list
Returns the current set of axioms.
A call axioms() returns the current list of axioms.
- FAILURE CONDITIONS
Under normal circumstances, the list of axioms will be as follows, containing
the axioms of infinity, choice and extensionality.
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'.
val it : thm list =
[|- ?f. ONE_ONE f /\ ~ONTO f; |- !P x. P x ==> P ((@) P);
|- !t. (\x. t x) = t]
- SEE ALSO
define, definitions, new_axiom, new_definition, the_definitions.