# HG changeset patch
# User nipkow
# Date 1072129958 -3600
# Node ID d3e98d53533c3259fd56757f7a01a85b7b6f34e5
# Parent  314da085adf3b616e966744ed4c620f549d1d9fc
Updated proofs due to changes in Set.thy.

diff -r 314da085adf3 -r d3e98d53533c src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Mon Dec 22 18:29:20 2003 +0100
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Mon Dec 22 22:52:38 2003 +0100
@@ -901,8 +901,6 @@
   apply(case_tac ys,simp+)
  apply clarify
  apply(case_tac ys,simp+)
- apply(drule last_length2,simp)
-apply simp
 done
 
 subsubsection{* Soundness of the While rule *}
@@ -950,18 +948,6 @@
 apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
 done
 
-lemma last_append2:"ys\<noteq>[] \<Longrightarrow> last (xs@ys)=(last ys)"
-apply(frule last_length2)
-apply simp
-apply(subgoal_tac "xs@ys\<noteq>[]")
-apply(drule last_length2)
-back
-apply simp
-apply(drule_tac xs=xs in last_append)
-apply simp
-apply simp
-done
-
 lemma While_sound_aux [rule_format]: 
   "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
    stable pre rely;  stable post rely; x \<in> cptn_mod \<rbrakk>