src/HOL/Wellfounded.thy
changeset 46882 6242b4bc05bc
parent 46664 1f6c140f9c72
child 46883 eec472dae593
     1.1 --- a/src/HOL/Wellfounded.thy	Sun Mar 11 22:06:13 2012 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Mon Mar 12 15:11:24 2012 +0100
     1.3 @@ -299,8 +299,7 @@
     1.4  lemma wfP_SUP:
     1.5    "\<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)"
     1.6    apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred])
     1.7 -  apply (simp_all add: inf_set_def)
     1.8 -  apply auto
     1.9 +  apply simp_all
    1.10    done
    1.11  
    1.12  lemma wf_Union: