Andreas@48041: (* Author: Andreas Lochbihler, KIT *) Andreas@48041: wenzelm@60500: section \Pretty syntax for almost everywhere constant functions\ Andreas@48041: wenzelm@51542: theory FinFun_Syntax wenzelm@51542: imports FinFun wenzelm@51542: begin Andreas@48041: Andreas@48041: type_notation Andreas@48041: finfun ("(_ =>f /_)" [22, 21] 21) Andreas@48041: Andreas@48041: type_notation (xsymbols) Andreas@48041: finfun ("(_ \f /_)" [22, 21] 21) Andreas@48041: Andreas@48041: notation Andreas@48041: finfun_const ("K$/ _" [0] 1) and Andreas@48041: finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and Andreas@48041: finfun_apply (infixl "$" 999) and Andreas@48041: finfun_comp (infixr "o$" 55) and Andreas@48041: finfun_comp2 (infixr "$o" 55) and Andreas@48041: finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000) Andreas@48041: Andreas@48041: notation (xsymbols) Andreas@48041: finfun_comp (infixr "\$" 55) and Andreas@48041: finfun_comp2 (infixr "$\" 55) Andreas@48041: Andreas@48041: end