From 2a8ad9f439327acab576ebe510ed7afbd19b8db2 Mon Sep 17 00:00:00 2001 From: rajames Date: Fri, 6 Nov 2026 02:05:37 +0000 Subject: [PATCH] logs: Isabelle/HOL proof build of 4cef0431 -- passed 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 Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2 --- logs/20261106-015650/isabelle/isabelle-20261106-015650.log | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 logs/20261106-015650/isabelle/isabelle-20261106-015650.log diff --git a/logs/20261106-015650/isabelle/isabelle-20261106-015650.log b/logs/20261106-015650/isabelle/isabelle-20261106-015650.log new file mode 100644 index 00000000..51e36560 --- /dev/null +++ b/logs/20261106-015650/isabelle/isabelle-20261106-015650.log @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:bef8f1a76d4f5e531ddad332c0e273b91ac86c632041ce5d3a45a371aa80cbf3 +size 26320