src/HOL/Wellfounded.thy
changeset 32205 49db434c157f
parent 31775 2b04504fcb69
child 32235 8f9b8d14fc9f
     1.1 --- a/src/HOL/Wellfounded.thy	Sat Jul 25 18:44:54 2009 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Sat Jul 25 18:44:55 2009 +0200
     1.3 @@ -187,8 +187,12 @@
     1.4  lemma wf_empty [iff]: "wf({})"
     1.5    by (simp add: wf_def)
     1.6  
     1.7 -lemmas wfP_empty [iff] =
     1.8 -  wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq]
     1.9 +lemma wfP_empty [iff]:
    1.10 +  "wfP (\<lambda>x y. False)"
    1.11 +proof -
    1.12 +  have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2])
    1.13 +  then show ?thesis by (simp add: bot_fun_eq bot_bool_eq)
    1.14 +qed
    1.15  
    1.16  lemma wf_Int1: "wf r ==> wf (r Int r')"
    1.17    apply (erule wf_subset)