changeset 5780 | 0187f936685a |
parent 5492 | d9fc3457554e |
child 5931 | 325300576da7 |
--- a/src/HOL/Set.thy Fri Oct 30 10:43:12 1998 +0100 +++ b/src/HOL/Set.thy Fri Oct 30 10:45:08 1998 +0100 @@ -18,7 +18,7 @@ set :: (term) term instance - set :: (term) {ord, minus, power} (* only ('a * 'a) set should be in power! *) + set :: (term) {ord, minus} syntax "op :" :: ['a, 'a set] => bool ("op :")