equal
deleted
inserted
replaced
10 *) |
10 *) |
11 |
11 |
12 Store = Conform + |
12 Store = Conform + |
13 |
13 |
14 syntax |
14 syntax |
15 value :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ \\<And> _") |
15 map_apply :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ !! _") |
16 translations |
16 translations |
17 "t \\<And> x" == "the (t x)" |
17 "t !! x" == "the (t x)" |
18 |
18 |
19 constdefs |
19 constdefs |
20 newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a" |
20 newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a" |
21 "newref s \\<equiv> \\<epsilon>v. s v = None" |
21 "newref s \\<equiv> \\<epsilon>v. s v = None" |
22 |
22 |