changeset 22886 | cdff6ef76009 |
parent 22845 | 5f9138bcb3d7 |
child 23738 | 3a801ffdc58c |
--- a/src/HOL/Fun.thy Wed May 09 07:53:04 2007 +0200 +++ b/src/HOL/Fun.thy Wed May 09 07:53:06 2007 +0200 @@ -7,12 +7,12 @@ header {* Notions about functions *} theory Fun -imports Set Code_Generator +imports Set begin constdefs fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" - [code func]: "fun_upd f a b == % x. if x=a then b else f x" + "fun_upd f a b == % x. if x=a then b else f x" nonterminals updbinds updbind