Isabelle202X cleanup

[kape1395]

Reorganized Isabelle's build sessions to use a single root file.

[kape1395]

@muenchnerkindl, the file isabelle/examples/AtomicBakeryG.thy has failing steps.
Maybe you could check if the proof needs to be updated or if the main theory needs to be fixed.

[kape1395]

At least some of the failures are also caused by Nat/Int. E.g.

    with type have n: "num[i] ∈ Nat" (* by (auto simp: TypeOK_def) *)
    proof -
      have "num ∈ [ProcSet → Nat]" sorry
      thus "num[i] ∈ Nat" by auto
    qed

Here thus "num[i] ∈ Nat" by auto fails with

Failed to finish proof:
goal (2 subgoals):
 1. num ∈ [ProcSet → Nat] ⟹ num[i] ∈ Int
 2. num ∈ [ProcSet → Nat] ⟹ 0 ≤ num[i]

@muenchnerkindl, maybe it's worth removing the Nat -> Int rewrite and proving the Nat properties explicitly?

[kape1395]

@muenchnerkindl, I have excluded AtomicBakeryG.thy from the test cases for now. Can I merge it as is?