section ‹dGL Formalization› theory "Differential_Game_Logic" imports Complex_Main "Lib" "Identifiers" "Syntax" "Denotational_Semantics" "Static_Semantics" "Coincidence" "USubst" "Axioms" begin text ‹This formalization of Differential Game Logic 🌐‹http://arxiv.org/abs/1902.07230› \cite{DBLP:conf/cade/Platzer19} consists of the syntax, denotational semantics, static semantics, uniform substitution lemmas, uniform substitution soundness proofs, and soundness proofs for axioms.› end