src/HOL/Trancl.ML
changeset 6162 484adda70b65
parent 5771 7c2c8cf20221
child 6856 0364007b4bb3
     1.1 --- a/src/HOL/Trancl.ML	Fri Jan 29 16:23:56 1999 +0100
     1.2 +++ b/src/HOL/Trancl.ML	Fri Jan 29 16:26:12 1999 +0100
     1.3 @@ -312,7 +312,7 @@
     1.4  \     ==> P(a)";
     1.5  by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
     1.6   by (resolve_tac prems 1);
     1.7 - be converseD 1;
     1.8 + by (etac converseD 1);
     1.9  by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
    1.10  qed "converse_trancl_induct";
    1.11