# 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="\<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>