1signature EXPANSION_INTERFACE = 2sig 3type T 4 5val expand_term : 6 Lazy_Eval.eval_ctxt -> term -> Asymptotic_Basis.basis -> T * Asymptotic_Basis.basis 7val expand_terms : 8 Lazy_Eval.eval_ctxt -> term list -> Asymptotic_Basis.basis -> T list * Asymptotic_Basis.basis 9 10val prove_nhds : Lazy_Eval.eval_ctxt -> T * Asymptotic_Basis.basis -> thm 11val prove_at_infinity : Lazy_Eval.eval_ctxt -> T * Asymptotic_Basis.basis -> thm 12val prove_at_top : Lazy_Eval.eval_ctxt -> T * Asymptotic_Basis.basis -> thm 13val prove_at_bot : Lazy_Eval.eval_ctxt -> T * Asymptotic_Basis.basis -> thm 14val prove_at_0 : Lazy_Eval.eval_ctxt -> T * Asymptotic_Basis.basis -> thm 15val prove_at_right_0 : Lazy_Eval.eval_ctxt -> T * Asymptotic_Basis.basis -> thm 16val prove_at_left_0 : Lazy_Eval.eval_ctxt -> T * Asymptotic_Basis.basis -> thm 17val prove_eventually_nonzero : Lazy_Eval.eval_ctxt -> T * Asymptotic_Basis.basis -> thm 18 19val prove_eventually_less : Lazy_Eval.eval_ctxt -> T * T * Asymptotic_Basis.basis -> thm 20val prove_eventually_greater : Lazy_Eval.eval_ctxt -> T * T * Asymptotic_Basis.basis -> thm 21 22val prove_smallo : Lazy_Eval.eval_ctxt -> T * T * Asymptotic_Basis.basis -> thm 23val prove_bigo : Lazy_Eval.eval_ctxt -> T * T * Asymptotic_Basis.basis -> thm 24val prove_bigtheta : Lazy_Eval.eval_ctxt -> T * T * Asymptotic_Basis.basis -> thm 25val prove_asymp_equiv : Lazy_Eval.eval_ctxt -> T * T * Asymptotic_Basis.basis -> thm 26 27end