diff -r 7544966fa07d -r 7195c9b0423f src/HOL/MicroJava/J/State.thy
--- 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