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 haftmann
Mon, 06 Jun 2016 21:28:46 +0200
changeset 63239 d562c9948dee
parent 60500 903bb1495239
permissions -rw-r--r--
explicit tagging of code equations de-baroquifies interface

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

Cardinal notations.
*)

section \<open>Cardinal Notations\<close>

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