[llm] LOAD -noproof: admit the prefix's lemmas instead of proving them - #1117

Merged

strub merged 3 commits into

llm-interactivefrom

llm-interactive-fast-load

Sep 7, 2026

Commits on Sep 7, 2026

[llm] LOAD -noproof: admit the prefix's lemmas instead of proving them

bgregoir
and
claude
committed
a77f2a7
[llm] keep elaborated theories across a LOAD, so reloading is cheap

bgregoir
and
claude
committed
f017b9c
[llm] STRICT: stop the session at a failure instead of drifting past it

bgregoir
and
claude
committed
c9751bd