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