blanchet@49263: (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
blanchet@49263:     Author:     Jasmin Blanchette, TU Muenchen
blanchet@49263: 
blanchet@49263: Sledgehammer's machine-learning-based relevance filter (MaSh).
blanchet@49263: *)
blanchet@49263: 
blanchet@49263: signature SLEDGEHAMMER_FILTER_MASH =
blanchet@49263: sig
blanchet@49263: end;
blanchet@49263: 
blanchet@49263: structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
blanchet@49263: struct
blanchet@49263: end;