1.1 --- a/src/HOL/List.thy Sun Nov 10 10:02:34 2013 +0100
1.2 +++ b/src/HOL/List.thy Sun Nov 10 15:05:06 2013 +0100
1.3 @@ -5514,15 +5514,15 @@
1.4 text{* Accessible part and wellfoundedness: *}
1.5
1.6 lemma Cons_acc_listrel1I [intro!]:
1.7 - "x \<in> acc r \<Longrightarrow> xs \<in> acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> acc (listrel1 r)"
1.8 -apply (induct arbitrary: xs set: acc)
1.9 + "x \<in> Wellfounded.acc r \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> Wellfounded.acc (listrel1 r)"
1.10 +apply (induct arbitrary: xs set: Wellfounded.acc)
1.11 apply (erule thin_rl)
1.12 apply (erule acc_induct)
1.13 apply (rule accI)
1.14 apply (blast)
1.15 done
1.16
1.17 -lemma lists_accD: "xs \<in> lists (acc r) \<Longrightarrow> xs \<in> acc (listrel1 r)"
1.18 +lemma lists_accD: "xs \<in> lists (Wellfounded.acc r) \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r)"
1.19 apply (induct set: lists)
1.20 apply (rule accI)
1.21 apply simp
1.22 @@ -5530,8 +5530,8 @@
1.23 apply (fast dest: acc_downward)
1.24 done
1.25
1.26 -lemma lists_accI: "xs \<in> acc (listrel1 r) \<Longrightarrow> xs \<in> lists (acc r)"
1.27 -apply (induct set: acc)
1.28 +lemma lists_accI: "xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> xs \<in> lists (Wellfounded.acc r)"
1.29 +apply (induct set: Wellfounded.acc)
1.30 apply clarify
1.31 apply (rule accI)
1.32 apply (fastforce dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)