use predefined preferences categories;
authorwenzelm
Sat, 25 Apr 2009 21:28:05 +0200
changeset 309837882a1268a48
parent 30982 6b9b93816b30
child 30984 e6349035148a
use predefined preferences categories;
src/HOL/Tools/atp_manager.ML
     1.1 --- a/src/HOL/Tools/atp_manager.ML	Sat Apr 25 21:28:05 2009 +0200
     1.2 +++ b/src/HOL/Tools/atp_manager.ML	Sat Apr 25 21:28:05 2009 +0200
     1.3 @@ -51,15 +51,17 @@
     1.4  fun set_timeout time = CRITICAL (fn () => timeout := time);
     1.5  
     1.6  val _ =
     1.7 -  ProofGeneralPgip.add_preference "Proof"
     1.8 +  ProofGeneralPgip.add_preference Preferences.category_proof
     1.9      (Preferences.string_pref atps
    1.10        "ATP: provers" "Default automatic provers (separated by whitespace)");
    1.11  
    1.12 -val _ = ProofGeneralPgip.add_preference "Proof"
    1.13 +val _ =
    1.14 +  ProofGeneralPgip.add_preference Preferences.category_proof
    1.15      (Preferences.int_pref max_atps
    1.16        "ATP: maximum number" "How many provers may run in parallel");
    1.17  
    1.18 -val _ = ProofGeneralPgip.add_preference "Proof"
    1.19 +val _ =
    1.20 +  ProofGeneralPgip.add_preference Preferences.category_proof
    1.21      (Preferences.int_pref timeout
    1.22        "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
    1.23