Re: [isabelle] Isabelle
Induction cannot be broken down into smaller steps. It is a primitive concept.
On 30 Sep 2014, at 13:15, mahmoud abdelazim <m.abdelazim at icloud.com> wrote:
> i am user of Isabelle and i am trying to proof a theorem for example :
> theorem rev_rev [simp]: "rev(rev xs) = xs"
> apply(induct_tac xs)
> The steps of auto could be done using separate steps?
> The steps of induct_tac could be done using separate steps?
> please provide an example
This archive was generated by a fusion of
Pipermail (Mailman edition) and