added hint on fun_sum
authoroheimb
Fri Jul 14 16:27:45 2000 +0200 (2000-07-14)
changeset 93409666f78ecfab
parent 9339 0d8b0eb2932d
child 9341 40bab6613000
added hint on fun_sum
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Fri Jul 14 16:27:42 2000 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Jul 14 16:27:45 2000 +0200
     1.3 @@ -28,6 +28,13 @@
     1.4  defs
     1.5    fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
     1.6  
     1.7 +(* Hint: to define the sum of two functions (or maps), use sum_case.
     1.8 +         A nice infix syntax could be defined (in Datatype.thy or below) by
     1.9 +consts
    1.10 +  fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
    1.11 +translations
    1.12 + "fun_sum" == "sum_case"
    1.13 +*)
    1.14    
    1.15  constdefs
    1.16    id ::  'a => 'a