src/Tools/auto_solve.ML
changeset 33889 4328de748fb2
parent 33301 1fe9fc908ec3
child 39138 53886463f559
equal deleted inserted replaced
33888:4e0da333f75b 33889:4328de748fb2
    25 val auto_time_limit = Unsynchronized.ref 2500;
    25 val auto_time_limit = Unsynchronized.ref 2500;
    26 val limit = Unsynchronized.ref 5;
    26 val limit = Unsynchronized.ref 5;
    27 
    27 
    28 val _ =
    28 val _ =
    29   ProofGeneralPgip.add_preference Preferences.category_tracing
    29   ProofGeneralPgip.add_preference Preferences.category_tracing
       
    30     (Preferences.nat_pref auto_time_limit
       
    31       "auto-solve-time-limit"
       
    32       "Time limit for seeking automatic solutions (in milliseconds).");
       
    33 
       
    34 val _ =
       
    35   ProofGeneralPgip.add_preference Preferences.category_tracing
    30   (setmp_CRITICAL auto true (fn () =>
    36   (setmp_CRITICAL auto true (fn () =>
    31     Preferences.bool_pref auto
    37     Preferences.bool_pref auto
    32       "auto-solve"
    38       "auto-solve"
    33       "Try to solve newly declared lemmas with existing theorems.") ());
    39       "Try to solve newly declared lemmas with existing theorems.") ());
    34 
       
    35 val _ =
       
    36   ProofGeneralPgip.add_preference Preferences.category_tracing
       
    37     (Preferences.nat_pref auto_time_limit
       
    38       "auto-solve-time-limit"
       
    39       "Time limit for seeking automatic solutions (in milliseconds).");
       
    40 
    40 
    41 
    41 
    42 (* hook *)
    42 (* hook *)
    43 
    43 
    44 val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
    44 val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>