src/ZF/ZF.ML
changeset 12372 cd3a09c7dac9
parent 11770 b6bb7a853dd2
child 12836 5ef96e63fba6
equal deleted inserted replaced
12371:80ca9058db95 12372:cd3a09c7dac9
    43 by (REPEAT (eresolve_tac prems 1)) ;
    43 by (REPEAT (eresolve_tac prems 1)) ;
    44 qed "rev_ballE";
    44 qed "rev_ballE";
    45 
    45 
    46 AddSIs [ballI];
    46 AddSIs [ballI];
    47 AddEs  [rev_ballE];
    47 AddEs  [rev_ballE];
    48 AddXDs [bspec];
       
    49 
    48 
    50 (*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
    49 (*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
    51 val ball_tac = dtac bspec THEN' assume_tac;
    50 val ball_tac = dtac bspec THEN' assume_tac;
    52 
    51 
    53 (*Trival rewrite rule;   (ALL x:A.P)<->P holds only if A is nonempty!*)
    52 (*Trival rewrite rule;   (ALL x:A.P)<->P holds only if A is nonempty!*)