src/HOL/WF_Rel.ML

 by (Blast_tac 1);
 qed "trans_finite_psubset";
 
 (*---------------------------------------------------------------------------
  * Wellfoundedness of finite acyclic relations
- * Cannot go into WF because it needs Finite
+ * Cannot go into WF because it needs Finite.
  *---------------------------------------------------------------------------*)
 
 Goal "finite r ==> acyclic r --> wf r";
 by (etac finite_induct 1);
  by (Blast_tac 1);

 qed "wf_iff_acyclic_if_finite";
 
 
 (*---------------------------------------------------------------------------
  * A relation is wellfounded iff it has no infinite descending chain
+ * Cannot go into WF because it needs type nat.
  *---------------------------------------------------------------------------*)
 
 Goalw [wf_eq_minimal RS eq_reflection]
   "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
 by (rtac iffI 1);