# HG changeset patch
# User streckem
# Date 1060347911 -7200
# Node ID 7195c9b0423f3ddabf4143d467cb99130b6222b4
# Parent  7544966fa07d6af092dbca7094bc7d02a31d2b19
added lemma c_hupd_fst

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