| changeset 57462 | dabd4516450d |
| parent 57431 | 02c408aed5ee |
| child 57532 | c7dc1f0a2b8a |
--- a/src/HOL/Tools/etc/options Tue Jul 01 16:47:10 2014 +0200 +++ b/src/HOL/Tools/etc/options Tue Jul 01 16:47:10 2014 +0200 @@ -36,4 +36,4 @@ -- "status of Z3 activation for non-commercial use (yes, no, unknown)" public option MaSh : string = "sml" - -- "machine learning engine to use by Sledgehammer (sml, nb, knn, none)" + -- "machine learning engine to use by Sledgehammer (nb_knn, nb, knn, none)"