LCF theorem prover

1. REDIRECT Logic for Computable Functions

{{R from modification}}