Re: [isabelle] clarsimp_all? explode_conj?



I have a clarsimp_all in my refinement framework, just import $AFP/Automatic_Refinement/Lib/Refine_Lib

apply (intro conjI) explodes all conjunctions

I heard the nicta guys had a allgoals eisbach combinator, but I never used it

Peter


-------- Original Message --------
Subject: [isabelle] clarsimp_all? explode_conj?
From: "JÃhnig, Nils Erik"
To: cl-isabelle-users at lists.cam.ac.uk
CC:


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.