# HG changeset patch
# User wenzelm
# Date 1344423080 -7200
# Node ID 18e76e2db6d4b316fb2c48363ad0676600ff7942
# Parent  f04320479ff923a9fc80b6636c44c3b9b85397fe
proper axiomatization of "mem" -- do not leave it formally unspecified;

diff -r f04320479ff9 -r 18e76e2db6d4 src/ZF/ZF.thy
--- 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