# HG changeset patch
# User krauss
# Date 1256595978 -3600
# Node ID 6fd85372981e2d3b52d756ec031e723da2650ca7
# Parent  885e1b7ecb333384ff13b3f3aeda6167553214a0
replaced (outdated) comments by explicit statements

diff -r 885e1b7ecb33 -r 6fd85372981e src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Oct 26 20:45:24 2009 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Oct 26 23:26:18 2009 +0100
@@ -59,14 +59,16 @@
 lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r"
   by (induct a arbitrary: x set: wf) blast
 
-(* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)
-lemmas wf_asym = wf_not_sym [elim_format]
+lemma wf_asym:
+  assumes "wf r" "(a, x) \<in> r"
+  obtains "(x, a) \<notin> r"
+  by (drule wf_not_sym[OF assms])
 
 lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r"
   by (blast elim: wf_asym)
 
-(* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
-lemmas wf_irrefl = wf_not_refl [elim_format]
+lemma wf_irrefl: assumes "wf r" obtains "(a, a) \<notin> r"
+by (drule wf_not_refl[OF assms])
 
 lemma wf_wellorderI:
   assumes wf: "wf {(x::'a::ord, y). x < y}"