1.1 --- a/src/HOL/IsaMakefile	Wed May 30 10:04:05 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed May 30 16:05:06 2012 +0200
     1.3 @@ -455,7 +455,7 @@
     1.4    Library/DAList.thy Library/Dlist.thy					\
     1.5    Library/Eval_Witness.thy						\
     1.6    Library/Extended_Real.thy Library/Extended_Nat.thy			\
     1.7 -  Library/FinFun.thy Library/Float.thy					\
     1.8 +  Library/FinFun.thy Library/FinFun_Syntax.thy Library/Float.thy	\
     1.9    Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
    1.10    Library/FrechetDeriv.thy Library/FuncSet.thy				\
    1.11    Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy	\

     2.1 --- a/src/HOL/Library/FinFun.thy	Wed May 30 10:04:05 2012 +0200
     2.2 +++ b/src/HOL/Library/FinFun.thy	Wed May 30 16:05:06 2012 +0200
     2.3 @@ -1443,4 +1443,24 @@
     2.4    (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
     2.5  by(simp add: finfun_to_list_update)
     2.6  
     2.7 +text {* Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again *}
     2.8 +
     2.9 +no_type_notation
    2.10 +  finfun ("(_ =>f /_)" [22, 21] 21)
    2.11 +
    2.12 +no_type_notation (xsymbols)
    2.13 +  finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    2.14 +
    2.15 +no_notation
    2.16 +  finfun_const ("K$/ _" [0] 1) and
    2.17 +  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
    2.18 +  finfun_apply (infixl "$" 999) and
    2.19 +  finfun_comp (infixr "o$" 55) and
    2.20 +  finfun_comp2 (infixr "$o" 55) and
    2.21 +  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
    2.22 +
    2.23 +no_notation (xsymbols) 
    2.24 +  finfun_comp (infixr "\<circ>$" 55) and
    2.25 +  finfun_comp2 (infixr "$\<circ>" 55)
    2.26 +
    2.27  end

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/FinFun_Syntax.thy	Wed May 30 16:05:06 2012 +0200
     3.3 @@ -0,0 +1,25 @@
     3.4 +(* Author: Andreas Lochbihler, KIT *)
     3.5 +
     3.6 +header {* Pretty syntax for almost everywhere constant functions *}
     3.7 +
     3.8 +theory FinFun_Syntax imports FinFun begin
     3.9 +
    3.10 +type_notation
    3.11 +  finfun ("(_ =>f /_)" [22, 21] 21)
    3.12 +
    3.13 +type_notation (xsymbols)
    3.14 +  finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    3.15 +
    3.16 +notation
    3.17 +  finfun_const ("K$/ _" [0] 1) and
    3.18 +  finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
    3.19 +  finfun_apply (infixl "$" 999) and
    3.20 +  finfun_comp (infixr "o$" 55) and
    3.21 +  finfun_comp2 (infixr "$o" 55) and
    3.22 +  finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
    3.23 +
    3.24 +notation (xsymbols) 
    3.25 +  finfun_comp (infixr "\<circ>$" 55) and
    3.26 +  finfun_comp2 (infixr "$\<circ>" 55)
    3.27 +
    3.28 +end
    3.29 \ No newline at end of file

     4.1 --- a/src/HOL/ex/FinFunPred.thy	Wed May 30 10:04:05 2012 +0200
     4.2 +++ b/src/HOL/ex/FinFunPred.thy	Wed May 30 16:05:06 2012 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4    Predicates modelled as FinFuns
     4.5  *}
     4.6  
     4.7 -theory FinFunPred imports "~~/src/HOL/Library/FinFun" begin
     4.8 +theory FinFunPred imports "~~/src/HOL/Library/FinFun_Syntax" begin
     4.9  
    4.10  text {* Instantiate FinFun predicates just like predicates *}
    4.11  

     5.1 --- a/src/HOL/ex/ROOT.ML	Wed May 30 10:04:05 2012 +0200
     5.2 +++ b/src/HOL/ex/ROOT.ML	Wed May 30 16:05:06 2012 +0200
     5.3 @@ -12,7 +12,7 @@
     5.4    "Hebrew",
     5.5    "Chinese",
     5.6    "Serbian",
     5.7 -  "~~/src/HOL/Library/FinFun"
     5.8 +  "~~/src/HOL/Library/FinFun_Syntax"
     5.9  ];
    5.10  
    5.11  use_thys [