Hello, Please how can I define and declare a tail recursion of factorial with Isabelle/HOL and tail recursive of Reverse with Isabelle/HOL Thanks -------------- next part -------------- An HTML attachment was scrubbed... URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140611/cd395cd9/attachment.html>