There are some CakeML-preamble-only tactics that were introduced for backward compatibility, e.g.: https://github.com/CakeML/cakeml/blob/master/misc/preamble.sml#L571 Would be nice to delete them completely from the codebase.
There are some CakeML-preamble-only tactics that were introduced for backward compatibility, e.g.:
https://github.com/CakeML/cakeml/blob/master/misc/preamble.sml#L571
Would be nice to delete them completely from the codebase.