equal
deleted
inserted
replaced
583 translations |
583 translations |
584 "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs" |
584 "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs" |
585 "f(x:=y)" == "CONST fun_upd f x y" |
585 "f(x:=y)" == "CONST fun_upd f x y" |
586 |
586 |
587 (* Hint: to define the sum of two functions (or maps), use case_sum. |
587 (* Hint: to define the sum of two functions (or maps), use case_sum. |
588 A nice infix syntax could be defined (in Datatype.thy or below) by |
588 A nice infix syntax could be defined by |
589 notation |
589 notation |
590 case_sum (infixr "'(+')"80) |
590 case_sum (infixr "'(+')"80) |
591 *) |
591 *) |
592 |
592 |
593 lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)" |
593 lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)" |