src/HOL/Library/Cardinal_Notations.thy
author blanchet
Mon, 20 Jan 2014 22:24:48 +0100
changeset 55087 252c7fec4119
parent 55078 558c9ceabaa1
child 55128 6e16d2dd4f14
permissions -rw-r--r--
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
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
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
     8
header {* Cardinal Notations *}
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
55070
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    20
  csum (infixr "+c" 65) and
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    21
  cprod (infixr "*c" 80) and
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    22
  cexp (infixr "^c" 90)
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    23
235c7661a96b rationalized dependencies
blanchet
parents:
diff changeset
    24
end