src/HOL/Transitive_Closure.ML
changeset 13704 854501b1e957
parent 12691 d21db58bcdc2
--- a/src/HOL/Transitive_Closure.ML	Sat Nov 09 00:12:25 2002 +0100
+++ b/src/HOL/Transitive_Closure.ML	Wed Nov 13 15:24:42 2002 +0100
@@ -37,10 +37,10 @@
 val trancl_converse = thm "trancl_converse";
 val trancl_converseD = thm "trancl_converseD";
 val trancl_converseI = thm "trancl_converseI";
-val trancl_def = thm "trancl_def";
 val trancl_induct = thm "trancl_induct";
 val trancl_insert = thm "trancl_insert";
 val trancl_into_rtrancl = thm "trancl_into_rtrancl";
+val trancl_into_trancl = thm "trancl_into_trancl";
 val trancl_into_trancl2 = thm "trancl_into_trancl2";
 val trancl_mono = thm "trancl_mono";
 val trancl_subset_Sigma = thm "trancl_subset_Sigma";