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