-
Heiko Becker authored
The functions can be used to generate HOL4 level certificates without stepping out of the logic and calling Daisy. As the functions are not verified their returned certificate should still be send through the checker pipeline. The sole benefit of the functions is that they can be used as in-logic generators for checker input.
724d0058