1signature regexpLib =
2sig
3
4  include Abbrev
5  type regexp = Regexp_Type.regexp
6
7  val regexp_compset : unit -> computeLib.compset
8
9  datatype evaluator = HOL | SML
10
11  val matcher : evaluator
12                  -> regexp
13                  -> {table:int vector vector,
14                      start:int,
15                      final:bool vector,
16                      matchfn : string -> bool,
17                      certificate: thm option}
18
19  val dfa_by_proof : string * regexp -> thm
20
21end