replaced (outdated) comments by explicit statements
authorkrauss
Mon Oct 26 23:26:18 2009 +0100 (2009-10-26)
changeset 332156fd85372981e
parent 33214 885e1b7ecb33
child 33216 7c61bc5d7310
replaced (outdated) comments by explicit statements
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Wellfounded.thy	Mon Oct 26 20:45:24 2009 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Mon Oct 26 23:26:18 2009 +0100
     1.3 @@ -59,14 +59,16 @@
     1.4  lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r"
     1.5    by (induct a arbitrary: x set: wf) blast
     1.6  
     1.7 -(* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)
     1.8 -lemmas wf_asym = wf_not_sym [elim_format]
     1.9 +lemma wf_asym:
    1.10 +  assumes "wf r" "(a, x) \<in> r"
    1.11 +  obtains "(x, a) \<notin> r"
    1.12 +  by (drule wf_not_sym[OF assms])
    1.13  
    1.14  lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r"
    1.15    by (blast elim: wf_asym)
    1.16  
    1.17 -(* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
    1.18 -lemmas wf_irrefl = wf_not_refl [elim_format]
    1.19 +lemma wf_irrefl: assumes "wf r" obtains "(a, a) \<notin> r"
    1.20 +by (drule wf_not_refl[OF assms])
    1.21  
    1.22  lemma wf_wellorderI:
    1.23    assumes wf: "wf {(x::'a::ord, y). x < y}"