--- a/src/HOL/Hoare_Parallel/RG_Tran.thy Thu Feb 14 16:17:36 2013 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Thu Feb 14 16:25:13 2013 +0100
@@ -715,9 +715,6 @@
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
done
-lemma less_Suc_0 [iff]: "(n < Suc 0) = (n = 0)"
-by auto
-
lemma aux_onlyif [rule_format]: "\<forall>xs s. (xs, s)#ys \<in> par_cptn \<longrightarrow>
(\<exists>clist. (length clist = length xs) \<and>
(xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#(snd i)) (zip xs clist) \<and>