Re: [isabelle] clarsimp_all? explode_conj?
explode conj: apply(intro conjI)
and clarsimp_all from $AFP/Automatic_Refinement/Lib/Refine_Util
are what I was looking for.
From: Peter Lammich <lammich at in.tum.de><mailto:lammich at in.tum.de>
Date: 18. August 2017 at 15:25:06
To: JÃhnig, Nils Erik <nils.jaehnig at tu-berlin.de><mailto:nils.jaehnig at tu-berlin.de>, cl-isabelle-users at lists.cam.ac.uk <cl-isabelle-users at lists.cam.ac.uk><mailto:cl-isabelle-users at lists.cam.ac.uk>
Subject: Re: [isabelle] clarsimp_all? explode_conj?
Sorry, the theory name for clarsimp_all is Refine_Util
-------- Original Message --------
Subject: [isabelle] clarsimp_all? explode_conj?
From: "JÃhnig, Nils Erik"
To: cl-isabelle-users at lists.cam.ac.uk
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and