equal
deleted
inserted
replaced
82 "apply" :: "[i, i] => i" (infixl "`" 90) --{*function application*} |
82 "apply" :: "[i, i] => i" (infixl "`" 90) --{*function application*} |
83 "Int" :: "[i, i] => i" (infixl "Int" 70) --{*binary intersection*} |
83 "Int" :: "[i, i] => i" (infixl "Int" 70) --{*binary intersection*} |
84 "Un" :: "[i, i] => i" (infixl "Un" 65) --{*binary union*} |
84 "Un" :: "[i, i] => i" (infixl "Un" 65) --{*binary union*} |
85 Diff :: "[i, i] => i" (infixl "-" 65) --{*set difference*} |
85 Diff :: "[i, i] => i" (infixl "-" 65) --{*set difference*} |
86 Subset :: "[i, i] => o" (infixl "<=" 50) --{*subset relation*} |
86 Subset :: "[i, i] => o" (infixl "<=" 50) --{*subset relation*} |
|
87 |
|
88 axiomatization |
87 mem :: "[i, i] => o" (infixl ":" 50) --{*membership relation*} |
89 mem :: "[i, i] => o" (infixl ":" 50) --{*membership relation*} |
88 |
90 |
89 abbreviation |
91 abbreviation |
90 not_mem :: "[i, i] => o" (infixl "~:" 50) --{*negated membership relation*} |
92 not_mem :: "[i, i] => o" (infixl "~:" 50) --{*negated membership relation*} |
91 where "x ~: y == ~ (x : y)" |
93 where "x ~: y == ~ (x : y)" |