src/HOL/WF.ML
changeset 4746 a5dcd7e4a37d
parent 4686 74a12e86b20b
child 4750 f83cd6a06676
--- a/src/HOL/WF.ML	Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/WF.ML	Mon Mar 16 16:50:50 1998 +0100
@@ -144,8 +144,8 @@
 AddIffs [acyclic_insert];
 
 goalw WF.thy [acyclic_def] "acyclic(r^-1) = acyclic r";
-by (simp_tac (simpset() addsimps [trancl_inverse]) 1);
-qed "acyclic_inverse";
+by (simp_tac (simpset() addsimps [trancl_converse]) 1);
+qed "acyclic_converse";
 
 (** cut **)