src/HOL/Library/FinFun_Syntax.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 61955 e96292f32c3c
child 62390 842917225d56
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     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