--- a/src/HOL/MicroJava/J/State.thy Fri Aug 08 14:59:52 2003 +0200
+++ b/src/HOL/MicroJava/J/State.thy Fri Aug 08 15:05:11 2003 +0200
@@ -143,4 +143,7 @@
apply (simp (no_asm))
done
+lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x"
+by (simp add: c_hupd_def split_beta)
+
end