src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML

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