Re: [isabelle] apply proof method to all subgoals



Hi,

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.


Greetings,
Joachim

-- 
Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de

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



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