Renaming of a lemma
authorpaulson
Fri Apr 26 13:33:51 1996 +0200 (1996-04-26)
changeset 16925324be24a5fa
parent 1691 fbbd65c89c23
child 1693 7083f6b05423
Renaming of a lemma
src/ZF/ex/Comb.ML
     1.1 --- a/src/ZF/ex/Comb.ML	Fri Apr 26 13:30:26 1996 +0200
     1.2 +++ b/src/ZF/ex/Comb.ML	Fri Apr 26 13:33:51 1996 +0200
     1.3 @@ -177,9 +177,7 @@
     1.4  by (fast_tac (ZF_cs addIs [r_into_trancl]) 1);
     1.5  by (slow_best_tac (ZF_cs addSDs [spec RS mp]
     1.6                           addIs  [r_into_trancl, trans_trancl RS transD]) 1);
     1.7 -qed "diamond_trancl_lemma";
     1.8 -
     1.9 -val diamond_lemmaE = diamond_trancl_lemma RS spec RS mp RS exE;
    1.10 +val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
    1.11  
    1.12  val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)";
    1.13  by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
    1.14 @@ -187,7 +185,7 @@
    1.15  by (etac trancl_induct 1);
    1.16  by (ALLGOALS
    1.17      (slow_best_tac (ZF_cs addIs [r_into_trancl, trans_trancl RS transD]
    1.18 -                          addEs [major RS diamond_lemmaE])));
    1.19 +                          addEs [major RS diamond_strip_lemmaE])));
    1.20  qed "diamond_trancl";
    1.21  
    1.22