new_type : string * int -> unit
# new_type("set",0);; val it : unit = () # new_constant("mem",`:set->set->bool`);; val it : unit = () # parse_as_infix("mem",(11,"right"));; val it : unit = () # let ZF_EXT = new_axiom `(!z. z mem x <=> z mem y) ==> (x = y)`;; val ( ZF_EXT ) : thm = |- (!z. z mem x <=> z mem y) ==> x = y