1.5 26-05-2024: Version 3.4 of the Isabelle ITL proof library

• Deep embedding of PITL and QPITL is included to allow for proofs of theorems about them, notably that any PITL or QPITL formula can be rewritten in Guarded Normal Form (GNF) [2, 34].
• Added definition and lemmas for the time reversal operator, ported from the ITL v2.x series. Note only finite ITL formula can be reversed.
• The document structure is now report with four chapters: 1 Model: Intervals; 2 Shallow embedding of Finite and Infinite ITL; 3 Deep embedding of PITL; 4 Deep embedding of QPITL.