3 ms·

This should be possible when the underlying logics are similar (e.g. Isabelle/HOL and HOLight) but can be tricky if the logics are far apart (e.g. Isabelle/HOL

by mafribe 10y ago

This should be possible when the underlying logics are similar (e.g. Isabelle/HOL and HOLight) but can be tricky if the logics are far apart (e.g. Isabelle/HOL and Coq).