[LE] ================================================ AMAST Links 02 07

               Function definition in highter order logic
                             Konrad Slind

  A paper about a mechanization of the wellfounded recursion theorem is
available via URL: ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/
nipkow/slind/papers/wfrec.ps.Z

  It uses a formally proven wellfounded recursion theorem as the basis
upon which to build a function definition facility for Higher Order
Logic. This approach offers flexibility in the choice of wellfounded
relations used, the deferral of termination arguments, and automatic
isolation of termination conditions. Building on this platform, we
provide the ability to define recursive functions via pattern matching.
The system is parameterized and has already been instantiated to quite 
different theorem provers (HOL and Isabelle).