added Ferrante and Rackoff Algorithm -- by Amine Chaieb;

fixed handling of absolute urls

added the lemmas pt_fresh_aux and pt_fresh_aux_ineq (they are used in the proof of the strong induction principle) added code to nominal_atoms to collect these lemmas in "fresh_aux" instantiated for each atom type deleted the fresh_fun_eqvt from nominal_atoms, since fresh_fun is not used anymore in the recursion combinator

reactivated translations for less/less_eq;

added add_primrec_unchecked_i;

unchecked definitions;