equal
deleted
inserted
replaced
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 => |