diff -r 51dfdcd88e84 -r c503730efae5 etc/options --- a/etc/options Thu Jul 18 22:00:35 2013 +0200 +++ b/etc/options Thu Jul 18 22:18:20 2013 +0200 @@ -125,3 +125,13 @@ public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" + + +section "Miscellaneous Tools" + +public option find_theorems_limit : int = 40 + -- "limit of displayed results" + +public option find_theorems_tac_limit : int = 5 + -- "limit of tactic search for 'solves' criterion" +