proper axiomatization of "mem" -- do not leave it formally unspecified;

--- a/src/ZF/ZF.thy	Wed Aug 08 12:38:41 2012 +0200
+++ b/src/ZF/ZF.thy	Wed Aug 08 12:51:20 2012 +0200
@@ -84,6 +84,8 @@
   "Un"        :: "[i, i] => i"    (infixl "Un" 65) --{*binary union*}
   Diff        :: "[i, i] => i"    (infixl "-" 65) --{*set difference*}
   Subset      :: "[i, i] => o"    (infixl "<=" 50) --{*subset relation*}
+
+axiomatization
   mem         :: "[i, i] => o"    (infixl ":" 50) --{*membership relation*}
 
 abbreviation