Re: [isabelle] writing an Isar proof for multiple subgoals



On 17.07.2015 10:56, Gergely Buday wrote:
>   fix P x assume "â xa . x = xa â P" then show P by simp
> next
>   fix x xa assume "x = xa"
>   from this show "x = xa" by assumption

A small hint: You may call the fixed variables as you like, so

   fix P x assume "â y . x = y â P" then show P by simp

is also allowed (and may look nicer).




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