def_beta_conv.ml

[francoisthire]

Why this file has been comitted?

[gabrielhdt]

As far as I understand, this is needed by the hol light export (Emilie knows that better): it must be downloaded with hol light files. There should be a note somewhere in the documentation to explain that. And it should be moved to utils or something of the kind.