| changeset 8038 | a13c3b80d3d4 |
| parent 8034 | 6fc37b5c5e98 |
| child 10042 | 7164dc0d24d8 |
--- a/src/HOL/MicroJava/JVM/Store.thy Mon Nov 29 11:21:50 1999 +0100 +++ b/src/HOL/MicroJava/JVM/Store.thy Mon Nov 29 14:12:53 1999 +0100 @@ -11,11 +11,6 @@ Store = Conform + -syntax - map_apply :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ !! _") -translations - "t !! x" == "the (t x)" - constdefs newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a" "newref s \\<equiv> \\<epsilon>v. s v = None"