Skip to content

Copied the proof of the lemma REAL_EXP_BOUND_LEMMA from HOL light.

Heiko Beckerrequested to merge
bound_for_exp_t into master

Work done by @mtekriwa and @hbecker .

Merge request reports