src/HOL/Library/FinFun_Syntax.thy
author Christian Sternagel
Thu, 13 Dec 2012 13:11:38 +0100
changeset 50516 ed6b40d15d1c
parent 48041 d60f6b41bf2d
child 51542 738598beeb26
permissions -rw-r--r--
renamed "emb" to "list_hembeq"; make "list_hembeq" reflexive independent of the base order; renamed "sub" to "sublisteq"; dropped "transp_on" (state transitivity explicitly instead); no need to hide "sub" after renaming; replaced some ASCII symbols by proper Isabelle symbols; NEWS

(* Author: Andreas Lochbihler, KIT *)

header {* Pretty syntax for almost everywhere constant functions *}

theory FinFun_Syntax imports FinFun begin

type_notation
  finfun ("(_ =>f /_)" [22, 21] 21)

type_notation (xsymbols)
  finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)

notation
  finfun_const ("K$/ _" [0] 1) and
  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
  finfun_apply (infixl "$" 999) and
  finfun_comp (infixr "o$" 55) and
  finfun_comp2 (infixr "$o" 55) and
  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)

notation (xsymbols) 
  finfun_comp (infixr "\<circ>$" 55) and
  finfun_comp2 (infixr "$\<circ>" 55)

end