src/HOL/Library/FinFun.thy
changeset 48041 d60f6b41bf2d
parent 48038 72a8506dd59b
child 48051 53a0df441e20
     1.1 --- a/src/HOL/Library/FinFun.thy	Wed May 30 10:04:05 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Wed May 30 16:05:06 2012 +0200
     1.3 @@ -1443,4 +1443,24 @@
     1.4    (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
     1.5  by(simp add: finfun_to_list_update)
     1.6  
     1.7 +text {* Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again *}
     1.8 +
     1.9 +no_type_notation
    1.10 +  finfun ("(_ =>f /_)" [22, 21] 21)
    1.11 +
    1.12 +no_type_notation (xsymbols)
    1.13 +  finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    1.14 +
    1.15 +no_notation
    1.16 +  finfun_const ("K$/ _" [0] 1) and
    1.17 +  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
    1.18 +  finfun_apply (infixl "$" 999) and
    1.19 +  finfun_comp (infixr "o$" 55) and
    1.20 +  finfun_comp2 (infixr "$o" 55) and
    1.21 +  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
    1.22 +
    1.23 +no_notation (xsymbols) 
    1.24 +  finfun_comp (infixr "\<circ>$" 55) and
    1.25 +  finfun_comp2 (infixr "$\<circ>" 55)
    1.26 +
    1.27  end