# HG changeset patch # User haftmann # Date 1248540295 -7200 # Node ID 49db434c157fe4c7b0d1f2a4a0bd6b76b2b8db0c # Parent b330aa4d59cb40a784be9fd8e0c6d2b846320604 explicit is better than implicit diff -r b330aa4d59cb -r 49db434c157f src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Sat Jul 25 18:44:54 2009 +0200 +++ b/src/HOL/Wellfounded.thy Sat Jul 25 18:44:55 2009 +0200 @@ -187,8 +187,12 @@ lemma wf_empty [iff]: "wf({})" by (simp add: wf_def) -lemmas wfP_empty [iff] = - wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq] +lemma wfP_empty [iff]: + "wfP (\x y. False)" +proof - + have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2]) + then show ?thesis by (simp add: bot_fun_eq bot_bool_eq) +qed lemma wf_Int1: "wf r ==> wf (r Int r')" apply (erule wf_subset)