--- a/src/HOL/Set.thy Mon Sep 23 17:46:12 1996 +0200
+++ b/src/HOL/Set.thy Mon Sep 23 17:47:49 1996 +0200
@@ -32,14 +32,16 @@
inj, surj :: ('a => 'b) => bool (*inj/surjective*)
inj_onto :: ['a => 'b, 'a set] => bool
"``" :: ['a => 'b, 'a set] => ('b set) (infixr 90)
- ":" :: ['a, 'a set] => bool (infixl 50) (*membership*)
+ (*membership*)
+ "op :" :: ['a, 'a set] => bool ("(_/ : _)" [50,51] 50)
syntax
UNIV :: 'a set
- "~:" :: ['a, 'a set] => bool (infixl 50)
+ (*infix synatx for non-membership*)
+ "op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50,51] 50)
"@Finset" :: args => 'a set ("{(_)}")