src/HOL/Set.thy
changeset 15120 f0359f75682e
parent 15102 04b0e943fcc9
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Set.thy	Fri Aug 06 16:54:26 2004 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Aug 06 16:55:14 2004 +0200
     1.3 @@ -120,17 +120,30 @@
     1.4    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
     1.5    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
     1.6  
     1.7 -syntax (input)
     1.8 +syntax (xsymbols)
     1.9    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
    1.10    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
    1.11    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
    1.12    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
    1.13 -
    1.14 +(*
    1.15  syntax (xsymbols)
    1.16    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
    1.17    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
    1.18    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
    1.19    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
    1.20 +*)
    1.21 +syntax (latex output)
    1.22 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
    1.23 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
    1.24 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
    1.25 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
    1.26 +
    1.27 +text{* Note the difference between ordinary xsymbol syntax of indexed
    1.28 +unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
    1.29 +and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
    1.30 +former does not make the index expression a subscript of the
    1.31 +union/intersection symbol because this leads to problems with nested
    1.32 +subscripts in Proof General.  *}
    1.33  
    1.34  
    1.35  translations