Theory Differential_Game_Logic

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