changeset 46882 | 6242b4bc05bc |
parent 46664 | 1f6c140f9c72 |
child 46883 | eec472dae593 |
--- a/src/HOL/Wellfounded.thy Sun Mar 11 22:06:13 2012 +0100 +++ b/src/HOL/Wellfounded.thy Mon Mar 12 15:11:24 2012 +0100 @@ -299,8 +299,7 @@ lemma wfP_SUP: "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)" apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred]) - apply (simp_all add: inf_set_def) - apply auto + apply simp_all done lemma wf_Union: