src/HOL/Fun.thy
changeset 58111 82db9ad610b9
parent 57282 7da3e398804c
child 58195 1fee63e0377d
     1.1 --- a/src/HOL/Fun.thy	Mon Sep 01 16:17:46 2014 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Sep 01 16:17:46 2014 +0200
     1.3 @@ -585,7 +585,7 @@
     1.4    "f(x:=y)" == "CONST fun_upd f x y"
     1.5  
     1.6  (* Hint: to define the sum of two functions (or maps), use case_sum.
     1.7 -         A nice infix syntax could be defined (in Datatype.thy or below) by
     1.8 +         A nice infix syntax could be defined by
     1.9  notation
    1.10    case_sum  (infixr "'(+')"80)
    1.11  *)