src/HOL/Transitive_Closure.ML
changeset 13704 854501b1e957
parent 12691 d21db58bcdc2
     1.1 --- a/src/HOL/Transitive_Closure.ML	Sat Nov 09 00:12:25 2002 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.ML	Wed Nov 13 15:24:42 2002 +0100
     1.3 @@ -37,10 +37,10 @@
     1.4  val trancl_converse = thm "trancl_converse";
     1.5  val trancl_converseD = thm "trancl_converseD";
     1.6  val trancl_converseI = thm "trancl_converseI";
     1.7 -val trancl_def = thm "trancl_def";
     1.8  val trancl_induct = thm "trancl_induct";
     1.9  val trancl_insert = thm "trancl_insert";
    1.10  val trancl_into_rtrancl = thm "trancl_into_rtrancl";
    1.11 +val trancl_into_trancl = thm "trancl_into_trancl";
    1.12  val trancl_into_trancl2 = thm "trancl_into_trancl2";
    1.13  val trancl_mono = thm "trancl_mono";
    1.14  val trancl_subset_Sigma = thm "trancl_subset_Sigma";