(* $Id$ *) theory ZF_Specific imports ZF begin end