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