Re: [isabelle] apply proof method to all subgoals



On Sun, 17 Apr 2011, Makarius wrote:

notepad
begin
 fix z :: 'a and n :: nat
 have "A n z ==> B n z ==> C z"
 proof (induct n)
    ...

Here I meant to say (induct n arbitrary: z)


	Makarius





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