--- 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
--- a/src/HOL/SetInterval.thy Sat May 01 22:01:57 2004 +0200
+++ b/src/HOL/SetInterval.thy Sat May 01 22:04:14 2004 +0200
@@ -49,10 +49,10 @@
"@INTER_less" :: "nat => nat => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10)
syntax (xsymbols)
- "@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>\<^bsub>_ \<le> _\<^esub>/ _)" 10)
- "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>\<^bsub>_ < _\<^esub>/ _)" 10)
- "@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>\<^bsub>_ \<le> _\<^esub>/ _)" 10)
- "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>\<^bsub>_ < _\<^esub>/ _)" 10)
+ "@UNION_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
+ "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Union>()\<^bsub>_ < _\<^esub>/ _)" 10)
+ "@INTER_le" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
+ "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set" ("(3\<Inter>()\<^bsub>_ < _\<^esub>/ _)" 10)
translations
"UN i<=n. A" == "UN i:{..n}. A"