1.1 26-10-2026: Version 3.7 of the Isabelle ITL proof library

• added sfxbnd and pfxbnd which are restricted forms of existential quantification.
• added a formalisation of omega in terms of the nfusecat operator (infinite iterative fuse).
• added a formalisation of schopstar in terms of the nfusecat operator (finite iterative fuse).
• added the since operator.
• formalises the classification of temporal properties of Manna and Pnueli[167, 151]. The formalisation is at semantic level, i.e., in terms of sets of sequences of states.
• added the formalisation of upd which is used to model quantification in the deep embedding of temporal logics.
• added the formalisation of Fusion Logic.