Re: [isabelle] Tactic to force simplification?



On 04.08.2014 14:04, Holden Lee wrote:
> Often, I have something I want to prove, say
>
> f x = h x
>
> and there is a simplification I want to use, say
>
> P x => f x = g x
>
> I would like Isabelle to replace the goal
>
> 1. f x = h x
>
> by
>
> 1. P x
> 2. g x = h x.
apply (subst <rule>)

  -- Lars




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