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!
Andreas@48041
     1
(* Author: Andreas Lochbihler, KIT *)
Andreas@48041
     2
wenzelm@60500
     3
section \<open>Pretty syntax for almost everywhere constant functions\<close>
Andreas@48041
     4
wenzelm@51542
     5
theory FinFun_Syntax
wenzelm@51542
     6
imports FinFun
wenzelm@51542
     7
begin
Andreas@48041
     8
Andreas@48041
     9
type_notation
Andreas@48041
    10
  finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
Andreas@48041
    11
Andreas@48041
    12
notation
Andreas@48041
    13
  finfun_const ("K$/ _" [0] 1) and
Andreas@48041
    14
  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
Andreas@48041
    15
  finfun_apply (infixl "$" 999) and
wenzelm@61955
    16
  finfun_comp (infixr "\<circ>$" 55) and
wenzelm@61955
    17
  finfun_comp2 (infixr "$\<circ>" 55) and
Andreas@48041
    18
  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
Andreas@48041
    19
wenzelm@61955
    20
notation (ASCII)
wenzelm@61955
    21
  finfun_comp (infixr "o$" 55) and
wenzelm@61955
    22
  finfun_comp2 (infixr "$o" 55)
Andreas@48041
    23
Andreas@48041
    24
end