src/HOL/MicroJava/JVM/Store.ML
changeset 10042 7164dc0d24d8
parent 9998 09bf8fcd1c6e
     1.1 --- a/src/HOL/MicroJava/JVM/Store.ML	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/Store.ML	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -5,6 +5,6 @@
     1.4  *)
     1.5  
     1.6  Goalw [newref_def]
     1.7 - "hp x = None \\<longrightarrow> hp (newref hp) = None";
     1.8 + "hp x = None --> hp (newref hp) = None";
     1.9  by (fast_tac (claset() addIs [someI2_ex] addss (simpset())) 1);
    1.10  qed_spec_mp "newref_None";