
Andreas@48041: (* Author: Andreas Lochbihler, KIT *)
Andreas@48041: 
wenzelm@60500: section \<open>Pretty syntax for almost everywhere constant functions\<close>
Andreas@48041: 
wenzelm@51542: theory FinFun_Syntax
wenzelm@51542: imports FinFun
wenzelm@51542: begin
Andreas@48041: 
Andreas@48041: type_notation
Andreas@48041:   finfun ("(_ \<Rightarrow>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
wenzelm@61955:   finfun_comp (infixr "\<circ>$" 55) and
wenzelm@61955:   finfun_comp2 (infixr "$\<circ>" 55) and
Andreas@48041:   finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
Andreas@48041: 
wenzelm@61955: notation (ASCII)
wenzelm@61955:   finfun_comp (infixr "o$" 55) and
wenzelm@61955:   finfun_comp2 (infixr "$o" 55)
Andreas@48041: 
Andreas@48041: end



