Re: [isabelle] Substitute in the whole context



On 18.07.2014 13:02, Joachim Breitner wrote:
> Hi,
>
> I often see this pattern:
>
> I am in some isar context:
>         
>         case (CaseName a b c d)
>
> and one of the first few facts is finding out something about d:
>
>         from CaseName(..)
>         obtain e f where "d = (e,f)" <proof>
>
> and from now on, I would like to forget d, but I still have to unfold it
> in local facts and goals:
What about

   note CaseName = CaseName[unfolded `d = _`]

(although I'd probably use a different name)




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