src/HOL/Library/FinFun_Syntax.thy
author Andreas Lochbihler
Wed May 30 16:05:06 2012 +0200 (2012-05-30)
changeset 48041 d60f6b41bf2d
child 51542 738598beeb26
permissions -rw-r--r--
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas@48041
     1
(* Author: Andreas Lochbihler, KIT *)
Andreas@48041
     2
Andreas@48041
     3
header {* Pretty syntax for almost everywhere constant functions *}
Andreas@48041
     4
Andreas@48041
     5
theory FinFun_Syntax imports FinFun begin
Andreas@48041
     6
Andreas@48041
     7
type_notation
Andreas@48041
     8
  finfun ("(_ =>f /_)" [22, 21] 21)
Andreas@48041
     9
Andreas@48041
    10
type_notation (xsymbols)
Andreas@48041
    11
  finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
Andreas@48041
    12
Andreas@48041
    13
notation
Andreas@48041
    14
  finfun_const ("K$/ _" [0] 1) and
Andreas@48041
    15
  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
Andreas@48041
    16
  finfun_apply (infixl "$" 999) and
Andreas@48041
    17
  finfun_comp (infixr "o$" 55) and
Andreas@48041
    18
  finfun_comp2 (infixr "$o" 55) and
Andreas@48041
    19
  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
Andreas@48041
    20
Andreas@48041
    21
notation (xsymbols) 
Andreas@48041
    22
  finfun_comp (infixr "\<circ>$" 55) and
Andreas@48041
    23
  finfun_comp2 (infixr "$\<circ>" 55)
Andreas@48041
    24
Andreas@48041
    25
end