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