Definition of the function "recdef" which converts a recursion functional into the function defined by that functional.

Introduction

The idea here is that a of recursive equation is represented by a functional, which is obtained by abstracting the right hand side of the equation on the name of the function.
We want to define

Recursion Theorem

Proof Context

In this section I will create a decent proof context for recursive definitions, eventually.