src/HOL/MicroJava/JVM/Store.thy
changeset 10042 7164dc0d24d8
parent 8038 a13c3b80d3d4
child 10057 8c8d2d0d3ef8
     1.1 --- a/src/HOL/MicroJava/JVM/Store.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/Store.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  Store = Conform +  
     1.5  
     1.6  constdefs
     1.7 - newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
     1.8 - "newref s \\<equiv> \\<epsilon>v. s v = None"
     1.9 + newref :: "('a \\<leadsto> 'b) => 'a"
    1.10 + "newref s == SOME v. s v = None"
    1.11  
    1.12  end