src/HOL/Wellfounded.thy
changeset 44921 58eef4843641
parent 44144 74b3751ea271
child 44937 22c0857b8aab
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Sep 13 17:07:33 2011 -0700
     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_def bot_bool_def)
     1.8 +  then show ?thesis by (simp add: bot_fun_def)
     1.9  qed
    1.10  
    1.11  lemma wf_Int1: "wf r ==> wf (r Int r')"
    1.12 @@ -573,7 +573,7 @@
    1.13  
    1.14  theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"
    1.15    apply (rule wfPUNIVI)
    1.16 -  apply (induct_tac P x rule: accp_induct)
    1.17 +  apply (rule_tac P=P in accp_induct)
    1.18     apply blast
    1.19    apply blast
    1.20    done