# HG changeset patch
# User nipkow
# Date 1039169342 -3600
# Node ID ff140d072bc900ac8d41076ddf41f9bd0964243c
# Parent  e3cb04713384ae424df4f83b483b02c7a45459ef
*** empty log message ***

diff -r e3cb04713384 -r ff140d072bc9 src/HOL/Hoare/Pointers.thy
--- a/src/HOL/Hoare/Pointers.thy	Thu Dec 05 18:44:16 2002 +0100
+++ b/src/HOL/Hoare/Pointers.thy	Fri Dec 06 11:09:02 2002 +0100
@@ -104,6 +104,13 @@
 lemma List_Ref[simp]: "List h (Ref a) as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
 by(case_tac as, simp_all, fast)
 
+theorem notin_List_update[simp]:
+ "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
+apply(induct as)
+apply simp
+apply(clarsimp simp add:fun_upd_apply)
+done
+
 
 declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp]
 
@@ -127,13 +134,6 @@
 apply(fastsimp dest:List_hd_not_in_tl)
 done
 
-theorem notin_List_update[simp]:
- "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
-apply(induct as)
-apply simp
-apply(clarsimp simp add:fun_upd_apply)
-done
-
 subsection "Functional abstraction"
 
 constdefs