--- a/src/HOL/Hoare/Heap.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/Heap.thy Mon Sep 12 07:55:43 2011 +0200
@@ -32,15 +32,15 @@
lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
apply(case_tac xs)
-apply fastsimp
-apply fastsimp
+apply fastforce
+apply fastforce
done
lemma [simp]: "Path h (Ref a) as z =
(as = [] \<and> z = Ref a \<or> (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
apply(case_tac as)
-apply fastsimp
-apply fastsimp
+apply fastforce
+apply fastforce
done
lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
@@ -116,12 +116,12 @@
lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
apply (clarsimp simp add:in_set_conv_decomp)
apply(frule List_app[THEN iffD1])
-apply(fastsimp dest: List_unique)
+apply(fastforce dest: List_unique)
done
lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
apply(induct as, simp)
-apply(fastsimp dest:List_hd_not_in_tl)
+apply(fastforce dest:List_hd_not_in_tl)
done
lemma Path_is_List:
@@ -165,7 +165,7 @@
lemma list_Ref_conv[simp]:
"islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
apply(insert List_Ref[of h])
-apply(fastsimp simp:List_conv_islist_list)
+apply(fastforce simp:List_conv_islist_list)
done
lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"