src/HOL/SetInterval.thy
changeset 30372 96d508968153
parent 30242 aea5d7fa7ef5
child 30384 2f24531b2d3e
     1.1 --- a/src/HOL/SetInterval.thy	Mon Mar 09 09:24:50 2009 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Mar 09 09:38:36 2009 +0100
     1.3 @@ -59,13 +59,13 @@
     1.4    "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3INT _<=_./ _)" 10)
     1.5    "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3INT _<_./ _)" 10)
     1.6  
     1.7 -syntax (input)
     1.8 +syntax (xsymbols)
     1.9    "@UNION_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _\<le>_./ _)" 10)
    1.10    "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
    1.11    "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
    1.12    "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
    1.13  
    1.14 -syntax (xsymbols)
    1.15 +syntax (latex output)
    1.16    "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" 10)
    1.17    "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" 10)
    1.18    "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" 10)