src/HOL/Library/FinFun_Syntax.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 61384 9f5145281888
permissions -rw-r--r--
isabelle update_cartouches;
     1 (* Author: Andreas Lochbihler, KIT *)
     2 
     3 section \<open>Pretty syntax for almost everywhere constant functions\<close>
     4 
     5 theory FinFun_Syntax
     6 imports FinFun
     7 begin
     8 
     9 type_notation
    10   finfun ("(_ =>f /_)" [22, 21] 21)
    11 
    12 type_notation (xsymbols)
    13   finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    14 
    15 notation
    16   finfun_const ("K$/ _" [0] 1) and
    17   finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
    18   finfun_apply (infixl "$" 999) and
    19   finfun_comp (infixr "o$" 55) and
    20   finfun_comp2 (infixr "$o" 55) and
    21   finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
    22 
    23 notation (xsymbols) 
    24   finfun_comp (infixr "\<circ>$" 55) and
    25   finfun_comp2 (infixr "$\<circ>" 55)
    26 
    27 end