This sounds great! You seem to have done everything right.
Having the compatibility mode will make it easy to get everything working again
quickly, with the conversion to the new setup becoming a background task
(possibly to be combined with refactoring horrible old proofs).
Larry
On 14 Jan 20
Hi Thomas,
Am 14.01.2014 um 14:43 schrieb Thomas Sewell :
> To address Jasmin and Larry's concern, it is possible to switch back to the
> "compatibility mode" by setting a config variable in the context, or by
> calling the ML version with an extra parameter. Any legacy proof script can
> be r
