# 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