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