equal
deleted
inserted
replaced
137 section "Miscellaneous Tools" |
137 section "Miscellaneous Tools" |
138 |
138 |
139 public option find_theorems_limit : int = 40 |
139 public option find_theorems_limit : int = 40 |
140 -- "limit of displayed results" |
140 -- "limit of displayed results" |
141 |
141 |
142 public option find_theorems_tac_limit : int = 5 |
142 public option find_theorems_tactic_limit : int = 5 |
143 -- "limit of tactic search for 'solves' criterion" |
143 -- "limit of tactic search for 'solves' criterion" |
144 |
144 |
145 |
145 |
146 section "Completion" |
146 section "Completion" |
147 |
147 |