| author | blanchet |
| Wed, 11 Jul 2012 21:43:19 +0200 | |
| changeset 49263 | b6eb45a52c28 |
| child 49264 | 2bd242c56c90 |
| permissions | -rw-r--r-- |
| blanchet@49263 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML |
| blanchet@49263 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
| blanchet@49263 | 3 |
|
| blanchet@49263 | 4 |
Sledgehammer's machine-learning-based relevance filter (MaSh). |
| blanchet@49263 | 5 |
*) |
| blanchet@49263 | 6 |
|
| blanchet@49263 | 7 |
signature SLEDGEHAMMER_FILTER_MASH = |
| blanchet@49263 | 8 |
sig |
| blanchet@49263 | 9 |
end; |
| blanchet@49263 | 10 |
|
| blanchet@49263 | 11 |
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH = |
| blanchet@49263 | 12 |
struct |
| blanchet@49263 | 13 |
end; |