handle let expressions inside terms by unfolding (instead of raising an exception),
added examples to test this feature
(benchmark Isabelle
:extrafuns (
(uf_1 Int)
)
:assumption (not (< (+ uf_1 (+ (mod uf_1 2) (mod uf_1 2))) (+ uf_1 3)))
:formula true
)