ISA: Example in isabelle/examples/AtomicBakeryG.thy fails.

[kape1395]

This example fails after upgrading to Isabelle2024.
It might be because of the Nat/Int rewrite, but I'm unsure.

[kape1395]

The last commit this example was working is eed59fc,
It passes there with Isabelle2024, and a minor fix in the ROOT file

$ git diff
diff --git a/isabelle/examples/ROOT b/isabelle/examples/ROOT
index cbcd3fa..8033e83 100644
--- a/isabelle/examples/ROOT
+++ b/isabelle/examples/ROOT
@@ -6,7 +6,7 @@ Examples of using Isabelle/TLA+
 *)
 
 (* build the session (without a heap) using "isabelle build -D ." *)
-chapter "TLA+ Examples"
+chapter "TLA+Examples"
 session "TLA-Examples" = "TLA+" +
   options [document=pdf, document_output = "output", document_variants="document:outline=/proof"]

Tried to build it as follows in the isabelle/examples folder

~/Programs/Isabelle2024/bin/isabelle build -d ../ -D . -f -c

The next commit touching /isabelle/ is d44f1a1; the example fails here.

@muenchnerkindl, maybe that's useful for you.

[kape1395]

Resolved in #109 and #134 .