equal
deleted
inserted
replaced
9 Conform provides notions for the type safety proof of the Bytecode Verifier. |
9 Conform provides notions for the type safety proof of the Bytecode Verifier. |
10 *) |
10 *) |
11 |
11 |
12 Store = Conform + |
12 Store = Conform + |
13 |
13 |
14 syntax |
|
15 map_apply :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ !! _") |
|
16 translations |
|
17 "t !! x" == "the (t x)" |
|
18 |
|
19 constdefs |
14 constdefs |
20 newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a" |
15 newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a" |
21 "newref s \\<equiv> \\<epsilon>v. s v = None" |
16 "newref s \\<equiv> \\<epsilon>v. s v = None" |
22 |
17 |
23 end |
18 end |