src/HOL/Library/FinFun_Syntax.thy
author wenzelm
Mon Dec 28 21:47:32 2015 +0100 (2015-12-28)
changeset 61955 e96292f32c3c
parent 61384 9f5145281888
child 62390 842917225d56
permissions -rw-r--r--
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
     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 ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    11 
    12 notation
    13   finfun_const ("K$/ _" [0] 1) and
    14   finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
    15   finfun_apply (infixl "$" 999) and
    16   finfun_comp (infixr "\<circ>$" 55) and
    17   finfun_comp2 (infixr "$\<circ>" 55) and
    18   finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
    19 
    20 notation (ASCII)
    21   finfun_comp (infixr "o$" 55) and
    22   finfun_comp2 (infixr "$o" 55)
    23 
    24 end