| changeset 57566 | 0fb191472e4a |
| parent 57532 | c7dc1f0a2b8a |
| child 57659 | b246943b3aa3 |
--- a/src/HOL/Tools/etc/options Wed Jul 16 10:22:06 2014 +0200 +++ b/src/HOL/Tools/etc/options Wed Jul 16 17:57:27 2014 +0200 @@ -35,5 +35,5 @@ public option z3_non_commercial : string = "unknown" -- "status of Z3 activation for non-commercial use (yes, no, unknown)" -public option MaSh : string = "sml" +public option MaSh : string = "none" -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"