explicit is better than implicit
authorhaftmann
Sat Jul 25 18:44:55 2009 +0200 (2009-07-25)
changeset 3220549db434c157f
parent 32204 b330aa4d59cb
child 32206 b2e93cda0be8
explicit is better than implicit
src/HOL/Wellfounded.thy
     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)