diff -r 35b47e36e615 -r f83cd6a06676 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Tue Mar 24 15:46:08 1998 +0100
+++ b/src/HOL/WF.ML	Tue Mar 24 15:46:34 1998 +0100
@@ -131,6 +131,9 @@
 
 (*** acyclic ***)
 
+val acyclicI = prove_goalw WF.thy [acyclic_def] 
+"!!r. !x. (x, x) ~: r^+ ==> acyclic r" (K [atac 1]);
+
 goalw WF.thy [acyclic_def]
  "!!r. wf r ==> acyclic r";
 by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1);