src/HOL/MicroJava/JVM/Store.thy

--- a/src/HOL/MicroJava/JVM/Store.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -12,7 +12,7 @@
 Store = Conform +  
 
 constdefs
- newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
- "newref s \\<equiv> \\<epsilon>v. s v = None"
+ newref :: "('a \\<leadsto> 'b) => 'a"
+ "newref s == SOME v. s v = None"
 
 end