Skip to content

Copied the proof of the lemma REAL_EXP_BOUND_LEMMA from HOL light.

Heiko Becker requested to merge bound_for_exp_t into master

Work done by @mtekriwa and @hbecker .

Merge request reports