Mercurial Mercurial > repos > isabelle / file revision
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/Library/Cardinal_Notations.thy
author wenzelm
Sun, 02 Nov 2014 17:20:45 +0100
changeset 58881 b9556a055632
parent 55128 6e16d2dd4f14
child 60500 903bb1495239
permissions -rw-r--r--
modernized header;

(*  Title:      HOL/Library/Cardinal_Notations.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2013

Cardinal notations.
*)

section {* Cardinal Notations *}

theory Cardinal_Notations
imports Main
begin

notation
  ordLeq2 (infix "<=o" 50) and
  ordLeq3 (infix "\<le>o" 50) and
  ordLess2 (infix "<o" 50) and
  ordIso2 (infix "=o" 50) and
  card_of ("|_|") and
  BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
  BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
  BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)

abbreviation "cinfinite \<equiv> BNF_Cardinal_Arithmetic.cinfinite"
abbreviation "czero \<equiv> BNF_Cardinal_Arithmetic.czero"
abbreviation "cone \<equiv> BNF_Cardinal_Arithmetic.cone"
abbreviation "ctwo \<equiv> BNF_Cardinal_Arithmetic.ctwo"

end
isabelle