# HG changeset patch
# User wenzelm
# Date 1083441854 -7200
# Node ID b8d6c395c9e2b677ab67a51de2a9ce746c9cfc54
# Parent  e1eedc8cad37fa3974482bcbe865dd3388470d7e
improved subscript syntax;

diff -r e1eedc8cad37 -r b8d6c395c9e2 src/HOL/Set.thy
--- 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
diff -r e1eedc8cad37 -r b8d6c395c9e2 src/HOL/SetInterval.thy
--- 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"