Re: [isabelle] clarsimp_all? explode_conj?



Hi Nils,

there is a method 'clarsimp_all'.

Maybe
  apply (intro conjI)
achieves what you want from explode_conj?

Cheers,
Simon

On Fri, Aug 18, 2017 at 2:47 PM JÃhnig, Nils Erik <nils.jaehnig at tu-berlin.de>
wrote:

> Dear Isabelle Users,
>
>
> is there something like clarsimp_all, when auto is too much, but I still
> want to simplify all subgoals?
>
> And is there a nice way to implement "explode_conj", i.e. make a subgoal
> for each conjunct in the conclusion.
>
> Related: Is there a way to achieve this in Eisbach? From what I've read, I
> think it is not.
> In general I would be interested, if multiple subgoals can be addressed.
>
>
> Have a nice weekend
> Nils
>
>
>



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