search

Deducteam / Logipedia

An encyclopedia of proofs
56 stars 11 forks source link

def_beta_conv.ml #30

Open francoisthire opened 4 years ago

francoisthire commented 4 years ago

Why this file has been comitted?

gabrielhdt commented 4 years ago

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.