Re: [isabelle] Isabelle



Induction cannot be broken down into smaller steps. It is a primitive concept.
Larry Paulson


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)
>   apply(auto)
>   done
> 
> 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 MHonArc.