src/HOL/Library/Cardinal_Notations.thy
author blanchet
Mon, 20 Jan 2014 18:59:53 +0100
changeset 55078 558c9ceabaa1
parent 55075 b3d0a02a756d
child 55087 252c7fec4119
permissions -rw-r--r--
deactivate one more cardinal notation
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
55078
558c9ceabaa1 deactivate one more cardinal notation
blanchet
parents: 55075
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