src/HOL/Wellfounded.thy
changeset 41075 4bed56dc95fb
parent 40607 30d512bf47a7
child 41720 f749155883d7
     1.1 --- a/src/HOL/Wellfounded.thy	Wed Dec 08 13:34:50 2010 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Wed Dec 08 13:34:50 2010 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4    "wfP (\<lambda>x y. False)"
     1.5  proof -
     1.6    have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2])
     1.7 -  then show ?thesis by (simp add: bot_fun_eq bot_bool_eq)
     1.8 +  then show ?thesis by (simp add: bot_fun_def bot_bool_def)
     1.9  qed
    1.10  
    1.11  lemma wf_Int1: "wf r ==> wf (r Int r')"