| changeset 10042 | 7164dc0d24d8 |
| parent 8038 | a13c3b80d3d4 |
| child 10057 | 8c8d2d0d3ef8 |
| 10041:30693ebd16ae | 10042:7164dc0d24d8 |
|---|---|
10 *) |
10 *) |
11 |
11 |
12 Store = Conform + |
12 Store = Conform + |
13 |
13 |
14 constdefs |
14 constdefs |
15 newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a" |
15 newref :: "('a \\<leadsto> 'b) => 'a" |
16 "newref s \\<equiv> \\<epsilon>v. s v = None" |
16 "newref s == SOME v. s v = None" |
17 |
17 |
18 end |
18 end |