changeset 12338 | de0f4a63baa5 |
parent 12257 | e3f7d6fb55d7 |
child 12633 | ad9277743664 |
--- a/src/HOL/Set.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOL/Set.thy Sat Dec 01 18:52:32 2001 +0100 @@ -17,7 +17,7 @@ global typedecl 'a set -arities set :: ("term") "term" +arities set :: (type) type consts "{}" :: "'a set" ("{}") @@ -42,8 +42,8 @@ local -instance set :: ("term") ord .. -instance set :: ("term") minus .. +instance set :: (type) ord .. +instance set :: (type) minus .. subsection {* Additional concrete syntax *}