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