src/HOL/Library/FinFun_Syntax.thy
author Christian Sternagel
Wed Aug 29 12:23:14 2012 +0900 (2012-08-29)
changeset 49083 01081bca31b6
parent 48041 d60f6b41bf2d
child 51542 738598beeb26
permissions -rw-r--r--
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
     1 (* Author: Andreas Lochbihler, KIT *)
     2 
     3 header {* Pretty syntax for almost everywhere constant functions *}
     4 
     5 theory FinFun_Syntax imports FinFun begin
     6 
     7 type_notation
     8   finfun ("(_ =>f /_)" [22, 21] 21)
     9 
    10 type_notation (xsymbols)
    11   finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    12 
    13 notation
    14   finfun_const ("K$/ _" [0] 1) and
    15   finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
    16   finfun_apply (infixl "$" 999) and
    17   finfun_comp (infixr "o$" 55) and
    18   finfun_comp2 (infixr "$o" 55) and
    19   finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
    20 
    21 notation (xsymbols) 
    22   finfun_comp (infixr "\<circ>$" 55) and
    23   finfun_comp2 (infixr "$\<circ>" 55)
    24 
    25 end