[isabelle] Isabelle



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.