Implemented a HipSpec style loop for Isabelle which applies structural induction