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