# HG changeset patch
# User wenzelm
# Date 1208204996 -7200
# Node ID a053f13bc9da01866a6e2230d4e7bb2040e51592
# Parent  25c07f3878b0ea184adb3d2a9e6d16a55da73450
removed redundant hd_append variant;

diff -r 25c07f3878b0 -r a053f13bc9da src/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOLCF/IOA/ABP/Correctness.thy	Mon Apr 14 21:44:53 2008 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy	Mon Apr 14 22:29:56 2008 +0200
@@ -83,8 +83,8 @@
     "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
   apply simp
   apply (tactic {* auto_tac (@{claset},
-    HOL_ss addsplits [thm"list.split"]
-    addsimps (thms "reverse.simps" @ [thm "hd_append", thm "rev_red_not_nil"])) *})
+    HOL_ss addsplits [@{thm list.split}]
+    addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) *})
   done
 
 text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}
diff -r 25c07f3878b0 -r a053f13bc9da src/HOLCF/IOA/ABP/Lemmas.thy
--- a/src/HOLCF/IOA/ABP/Lemmas.thy	Mon Apr 14 21:44:53 2008 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.thy	Mon Apr 14 22:29:56 2008 +0200
@@ -39,9 +39,6 @@
 
 subsection {* Lists *}
 
-lemma hd_append: "hd(l@m) = (if l~=[] then hd(l) else hd(m))"
-  by (induct l) simp_all
-
 lemma cons_not_nil: "l ~= [] --> (? x xs. l = (x#xs))"
   by (induct l) simp_all