Re: [isabelle] introducing local names in proofs
The right way is to use a structured proof, where you have elements such as
def a \<equiv> "x+y+z"
let ?a = "x+y+z"
The former must be expanded explicitly, while the latter are mere abbreviations and expand automatically.
On 3 Mar 2011, at 10:17, Viorel Preoteasa wrote:
> 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