equal
deleted
inserted
replaced
19 |
19 |
20 val try0N = "try0"; |
20 val try0N = "try0"; |
21 val noneN = "none"; |
21 val noneN = "none"; |
22 |
22 |
23 datatype mode = Auto_Try | Try | Normal; |
23 datatype mode = Auto_Try | Try | Normal; |
24 |
|
25 val _ = |
|
26 ProofGeneral.preference_option ProofGeneral.category_tracing |
|
27 NONE |
|
28 @{system_option auto_methods} |
|
29 "auto-try0" |
|
30 "Try standard proof methods"; |
|
31 |
24 |
32 val default_timeout = seconds 5.0; |
25 val default_timeout = seconds 5.0; |
33 |
26 |
34 fun can_apply timeout_opt pre post tac st = |
27 fun can_apply timeout_opt pre post tac st = |
35 let val {goal, ...} = Proof.goal st in |
28 let val {goal, ...} = Proof.goal st in |