equal
deleted
inserted
replaced
23 convergence: real, |
23 convergence: real, |
24 theory_relevant: bool option, |
24 theory_relevant: bool option, |
25 follow_defs: bool, |
25 follow_defs: bool, |
26 isar_proof: bool, |
26 isar_proof: bool, |
27 shrink_factor: int, |
27 shrink_factor: int, |
28 sorts: bool, |
|
29 timeout: Time.time, |
28 timeout: Time.time, |
30 minimize_timeout: Time.time} |
29 minimize_timeout: Time.time} |
31 type problem = |
30 type problem = |
32 {subgoal: int, |
31 {subgoal: int, |
33 goal: Proof.context * (thm list * thm), |
32 goal: Proof.context * (thm list * thm), |
83 convergence: real, |
82 convergence: real, |
84 theory_relevant: bool option, |
83 theory_relevant: bool option, |
85 follow_defs: bool, |
84 follow_defs: bool, |
86 isar_proof: bool, |
85 isar_proof: bool, |
87 shrink_factor: int, |
86 shrink_factor: int, |
88 sorts: bool, |
|
89 timeout: Time.time, |
87 timeout: Time.time, |
90 minimize_timeout: Time.time} |
88 minimize_timeout: Time.time} |
91 |
89 |
92 type problem = |
90 type problem = |
93 {subgoal: int, |
91 {subgoal: int, |