1signature BoundedRewrites =
2sig
3
4  datatype control = UNBOUNDED | BOUNDED of int ref
5  type thm = Thm.thm
6  type controlled_thm = thm * control
7
8  val dest_tagged_rewrite : thm -> controlled_thm
9  val MK_BOUNDED : thm -> int -> thm
10  val DEST_BOUNDED : thm -> thm * int
11  val Ntimes : thm -> int -> thm
12  val Once : thm -> thm
13
14end
15