--- a/src/HOL/FixedPoint.thy Mon Mar 12 19:23:48 2007 +0100
+++ b/src/HOL/FixedPoint.thy Mon Mar 12 19:23:49 2007 +0100
@@ -39,10 +39,10 @@
"INFI A f == Inf (f ` A)"
syntax
- "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" 10)
- "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" 10)
- "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" 10)
- "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" 10)
+ "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10)
+ "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10)
+ "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10)
translations
"SUP x y. B" == "SUP x. SUP y. B"
--- a/src/HOL/Product_Type.thy Mon Mar 12 19:23:48 2007 +0100
+++ b/src/HOL/Product_Type.thy Mon Mar 12 19:23:49 2007 +0100
@@ -138,7 +138,7 @@
"_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')")
"" :: "pttrn => patterns" ("_")
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _")
- "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
+ "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
translations
"(x, y)" == "Pair x y"
--- a/src/HOL/Set.thy Mon Mar 12 19:23:48 2007 +0100
+++ b/src/HOL/Set.thy Mon Mar 12 19:23:49 2007 +0100
@@ -80,10 +80,10 @@
"@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})")
"@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")
"@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ :/ _./ _})")
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" 10)
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" 10)
+ "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
+ "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
+ "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10)
+ "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 10] 10)
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10)
"_Bex1" :: "pttrn => 'a set => bool => bool" ("(3EX! _:_./ _)" [0, 0, 10] 10)
@@ -125,16 +125,16 @@
syntax (xsymbols)
"@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \<in>/ _./ _})")
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" 10)
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" 10)
+ "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10)
+ "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
+ "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
+ "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
syntax (latex output)
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
+ "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+ "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+ "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
+ "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
text{*
Note the difference between ordinary xsymbol syntax of indexed