# HG changeset patch
# User oheimb
# Date 890750794 -3600
# Node ID f83cd6a06676a0101474cd10e6a2370cb9ba098f
# Parent  35b47e36e6151f87503c0de711d6c157ba3f72dc
added acyclicI

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);