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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55075
b3d0a02a756d dissolved BNF session
blanchet
parents: 55070
diff changeset
     1
(*  Title:      HOL/Library/Cardinal_Notations.thy
55070
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
     3
    Copyright   2013
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
     4
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
     5
Cardinal notations.
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
     6
*)
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
     7
58881
b9556a055632 modernized header;
wenzelm
parents: 55128
diff changeset
     8
section {* Cardinal Notations *}
55070
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
     9
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    10
theory Cardinal_Notations
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    11
imports Main
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    12
begin
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    13
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    14
notation
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    15
  ordLeq2 (infix "<=o" 50) and
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    16
  ordLeq3 (infix "\<le>o" 50) and
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    17
  ordLess2 (infix "<o" 50) and
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    18
  ordIso2 (infix "=o" 50) and
55087
252c7fec4119 renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
blanchet
parents: 55078
diff changeset
    19
  card_of ("|_|") and
55128
6e16d2dd4f14 hide 'csum' etc.
blanchet
parents: 55087
diff changeset
    20
  BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
6e16d2dd4f14 hide 'csum' etc.
blanchet
parents: 55087
diff changeset
    21
  BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
6e16d2dd4f14 hide 'csum' etc.
blanchet
parents: 55087
diff changeset
    22
  BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
6e16d2dd4f14 hide 'csum' etc.
blanchet
parents: 55087
diff changeset
    23
6e16d2dd4f14 hide 'csum' etc.
blanchet
parents: 55087
diff changeset
    24
abbreviation "cinfinite \<equiv> BNF_Cardinal_Arithmetic.cinfinite"
6e16d2dd4f14 hide 'csum' etc.
blanchet
parents: 55087
diff changeset
    25
abbreviation "czero \<equiv> BNF_Cardinal_Arithmetic.czero"
6e16d2dd4f14 hide 'csum' etc.
blanchet
parents: 55087
diff changeset
    26
abbreviation "cone \<equiv> BNF_Cardinal_Arithmetic.cone"
6e16d2dd4f14 hide 'csum' etc.
blanchet
parents: 55087
diff changeset
    27
abbreviation "ctwo \<equiv> BNF_Cardinal_Arithmetic.ctwo"
55070
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    28
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    29
end