src/HOL/Set.thy
changeset 14692 b8d6c395c9e2
parent 14565 c6dc17aab88a
child 14742 dde816115d6a
     1.1 --- a/src/HOL/Set.thy	Sat May 01 22:01:57 2004 +0200
     1.2 +++ b/src/HOL/Set.thy	Sat May 01 22:04:14 2004 +0200
     1.3 @@ -41,8 +41,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -instance set :: (type) ord ..
     1.8 -instance set :: (type) minus ..
     1.9 +instance set :: (type) "{ord, minus}" ..
    1.10  
    1.11  
    1.12  subsection {* Additional concrete syntax *}
    1.13 @@ -129,10 +128,10 @@
    1.14    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
    1.15  
    1.16  syntax (xsymbols)
    1.17 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>\<^bsub>_\<^esub>/ _)" 10)
    1.18 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>\<^bsub>_\<^esub>/ _)" 10)
    1.19 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.20 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.21 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>()\<^bsub>_\<^esub>/ _)" 10)
    1.22 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>()\<^bsub>_\<^esub>/ _)" 10)
    1.23 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.24 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.25  
    1.26  
    1.27  translations