1signature inline =
2sig
3  include Abbrev
4  val threshold : int ref
5  val unroll_limit : int ref
6
7  val size : term -> int
8  val identify_small_fun : term -> term
9  val once_expand_anonymous : thm -> thm
10  val expand_anonymous : thm -> thm
11  val mk_inline_rules : thm list -> thm list
12  val expand_named : thm list -> thm -> thm
13  val optimize : thm -> thm
14  val optimize_norm : thm list -> thm -> thm
15end