[isabelle] introducing local names in proofs
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] introducing local names in proofs
- From: Viorel Preoteasa <viorel.preoteasa at abo.fi>
- Date: Thu, 03 Mar 2011 12:17:37 +0200
- User-agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:184.108.40.206) Gecko/20110221 Lightning/1.0b2 Thunderbird/3.1.8
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and