Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SetInterval.thy
changeset 14692 b8d6c395c9e2
parent 14577 dbb95b825244
child 14846 b1fcade3880b
equal deleted inserted replaced
14691:e1eedc8cad37 14692:b8d6c395c9e2 
    47   "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
 
    47   "@UNION_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Union> _<_./ _)" 10)
 
    48   "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
 
    48   "@INTER_le"   :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _\<le>_./ _)" 10)
 
    49   "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
 
    49   "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
 
    50 
    50 
    51 syntax (xsymbols)
 
    51 syntax (xsymbols)
 
    52   "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>\<^bsub>_ \<le> _\<^esub>/ _)" 10)
 
    52   "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
 
    53   "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>\<^bsub>_ < _\<^esub>/ _)" 10)
 
    53   "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>()\<^bsub>_ < _\<^esub>/ _)" 10)
 
    54   "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>\<^bsub>_ \<le> _\<^esub>/ _)" 10)
 
    54   "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
 
    55   "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>\<^bsub>_ < _\<^esub>/ _)" 10)
 
    55   "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>()\<^bsub>_ < _\<^esub>/ _)" 10)
 
    56 
    56 
    57 translations
 
    57 translations
 
    58   "UN i<=n. A"  == "UN i:{..n}. A"
 
    58   "UN i<=n. A"  == "UN i:{..n}. A"
 
    59   "UN i<n. A"   == "UN i:{..n(}. A"
 
    59   "UN i<n. A"   == "UN i:{..n(}. A"
 
    60   "INT i<=n. A" == "INT i:{..n}. A"
 
    60   "INT i<=n. A" == "INT i:{..n}. A"
isabelle