# HG changeset patch # User wenzelm # Date 1360855513 -3600 # Node ID 4b3a062b65385ab8b408651a8b9ccaab2c070148 # Parent 6b2352111017bf930675706ab836e7c9411c64d1 obsolete; diff -r 6b2352111017 -r 4b3a062b6538 src/HOL/Hoare_Parallel/RG_Tran.thy --- 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="\j. ?H j \ (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]: "\xs s. (xs, s)#ys \ par_cptn \ (\clist. (length clist = length xs) \ (xs, s)#ys \ map (\i. (fst i,s)#(snd i)) (zip xs clist) \