[isabelle] introducing local names in proofs


In a proof I need to introduce some local names.
something like: a = x+y+z, b = a + x, ...
apply (subgoal_tac "\<exists> a b: a = x+y+z /\ b = a + x")
but this is simplified away by simp or safe.

Is there a way to achieve this goal?

Best regards,


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