isabelle build -v -D proof/ with Isabelle2025-2 (installed by make init):
HOL-Library built (0:04:42), then the StarForth session's 52 theories,
every one in proof/ROOT (0:00:24); 0:05:24 in all, exit 0, nothing
FAILED. No sorry or oops in any proof (the words appear only in
comments) and quick_and_dirty is not set. The two explicit axioms are
both in StarForth_Transition.thy, the inventory StarForth_Correctness.thy
gives.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
