# HG changeset patch
# User nipkow
# Date 1314363281 -7200
# Node ID 9ec0dcd351a442f9135e55c0fc8369c1c1aa1631
# Parent  369e8c28a61add7775521b5f905acd49353fb3c8# Parent  5e580115dfcd1f2e83e38af2cce98d267b690392
merged

diff -r 369e8c28a61a -r 9ec0dcd351a4 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Aug 26 10:25:13 2011 +0200
+++ b/src/HOL/List.thy	Fri Aug 26 14:54:41 2011 +0200
@@ -4703,7 +4703,7 @@
 qed
 
 
-text{* Accessible part of @{term listrel1} relations: *}
+text{* Accessible part and wellfoundedness: *}
 
 lemma Cons_acc_listrel1I [intro!]:
   "x \<in> acc r \<Longrightarrow> xs \<in> acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> acc (listrel1 r)"
@@ -4729,6 +4729,9 @@
 apply (fastsimp dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
 done
 
+lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
+by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff)
+
 
 subsubsection {* Lifting Relations to Lists: all elements *}