src/HOL/Tools/etc/options
changeset 57659 b246943b3aa3
parent 57566 0fb191472e4a
child 59753 d743e0e53f41
equal deleted inserted replaced
57658:f55c173a3cbc 57659:b246943b3aa3
    33   -- "ATPs will be interrupted after this time (in seconds)"
    33   -- "ATPs will be interrupted after this time (in seconds)"
    34 
    34 
    35 public option z3_non_commercial : string = "unknown"
    35 public option z3_non_commercial : string = "unknown"
    36   -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
    36   -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
    37 
    37 
    38 public option MaSh : string = "none"
    38 public option MaSh : string = "sml"
    39   -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"
    39   -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"