equal
deleted
inserted
replaced
6 |
6 |
7 signature TRY0 = |
7 signature TRY0 = |
8 sig |
8 sig |
9 val try0N : string |
9 val try0N : string |
10 val noneN : string |
10 val noneN : string |
11 val auto : bool Unsynchronized.ref |
|
12 val try0 : |
11 val try0 : |
13 Time.time option -> string list * string list * string list * string list |
12 Time.time option -> string list * string list * string list * string list |
14 -> Proof.state -> bool |
13 -> Proof.state -> bool |
15 val setup : theory -> theory |
14 val setup : theory -> theory |
16 end; |
15 end; |
22 |
21 |
23 val try0N = "try0" |
22 val try0N = "try0" |
24 |
23 |
25 val noneN = "none" |
24 val noneN = "none" |
26 |
25 |
27 val auto = Unsynchronized.ref false |
|
28 |
|
29 val _ = |
26 val _ = |
30 ProofGeneral.preference_bool ProofGeneral.category_tracing |
27 ProofGeneral.preference_option ProofGeneral.category_tracing |
31 NONE |
28 NONE |
32 auto |
29 @{option auto_try0} |
33 "auto-try0" |
30 "auto-try0" |
34 "Try standard proof methods" |
31 "Try standard proof methods" |
35 |
32 |
36 val default_timeout = seconds 5.0 |
33 val default_timeout = seconds 5.0 |
37 |
34 |
194 (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans) |
191 (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans) |
195 |
192 |
196 fun try_try0 auto = |
193 fun try_try0 auto = |
197 do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []) |
194 do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []) |
198 |
195 |
199 val setup = Try.register_tool (try0N, (30, auto, try_try0)) |
196 val setup = Try.register_tool (try0N, (30, @{option auto_try0}, try_try0)) |
200 |
197 |
201 end; |
198 end; |