| changeset 57532 | c7dc1f0a2b8a |
| parent 57462 | dabd4516450d |
| child 57566 | 0fb191472e4a |
--- a/src/HOL/Tools/etc/options Wed Jul 09 11:35:52 2014 +0200 +++ b/src/HOL/Tools/etc/options Wed Jul 09 11:35:52 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 (nb_knn, nb, knn, none)" + -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"