Re: [isabelle] apply proof method to all subgoals


Am Sonntag, den 10.04.2011, 15:19 +0100 schrieb Alex Katovsky:
> Is there some way that I can limit "apply safe", for example 
> something like "apply (safe only: conjI allI impI)"?

untested, but I recall that I used "apply (intro conjI allI impI)" in
such cases.


Joachim Breitner
  e-Mail: mail at
  ICQ#: 74513189
  Jabber-ID: nomeata at

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.