--- a/src/HOL/Set.thy Sat May 01 22:01:57 2004 +0200
+++ b/src/HOL/Set.thy Sat May 01 22:04:14 2004 +0200
@@ -41,8 +41,7 @@
local
-instance set :: (type) ord ..
-instance set :: (type) minus ..
+instance set :: (type) "{ord, minus}" ..
subsection {* Additional concrete syntax *}
@@ -129,10 +128,10 @@
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" 10)
syntax (xsymbols)
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>\<^bsub>_\<^esub>/ _)" 10)
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>\<^bsub>_\<^esub>/ _)" 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>\<^bsub>_\<in>_\<^esub>/ _)" 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>\<^bsub>_\<in>_\<^esub>/ _)" 10)
+ "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>()\<^bsub>_\<^esub>/ _)" 10)
+ "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>()\<^bsub>_\<^esub>/ _)" 10)
+ "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
+ "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
translations