--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Wed Nov 23 22:07:55 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Wed Nov 23 22:59:39 2011 +0100
@@ -84,8 +84,9 @@
"l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
apply simp
apply (tactic {* auto_tac (map_simpset (fn _ =>
- HOL_ss addsplits [@{thm list.split}]
- addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *})
+ HOL_ss
+ addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])
+ |> Splitter.add_split @{thm list.split}) @{context}) *})
done
text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}