proper system options for 'find_theorems';

guard unify tracing via visible status of global theory; find_theorems: back-patching of background theory to observe Context_Position.is_visible avoids spamming via auto solve_direct;

provide global operations as well;

tuned signature;

tuned;

explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;

immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;

merged

tuned message;

tuned signature;