equal
deleted
inserted
replaced
1 (* Title: HOL/UNITY/Update.thy |
1 (* Title: HOL/Update.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 Function updates: like the standard theory Map, but for ordinary functions |
6 Function updates: like theory Map, but for ordinary functions |
7 *) |
7 *) |
8 |
8 |
9 Update = Fun + |
9 Update = Fun + |
10 |
10 |
11 consts |
11 consts |
12 update :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
12 update :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
13 ("_/[_/:=/_]" [900,0,0] 900) |
13 ("_/[_/:=/_]" [900,0,0] 900) |
14 |
14 |
15 syntax (symbols) |
|
16 update :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
|
17 ("_/[_/\\<mapsto>/_]" [900,0,0] 900) |
|
18 |
|
19 defs |
15 defs |
20 update_def "f[a:=b] == %x. if x=a then b else f x" |
16 update_def "f[a:=b] == %x. if x=a then b else f x" |
21 |
17 |
22 end |
18 end |