Theory MSOinHOL_shallow_minimal

theory MSOinHOL_shallow_minimal
  imports MSOinHOL_faithfulness_locale
begin

text ‹Constants-only presentation: a global interpretation of the minimal
  shallow embedding.›

consts II :: ℐ  gg :: ℰ  GG :: 𝒢

global_interpretation MinS II gg GG .

text ‹Re-introduce the locale-internal notation at the global level.›

notation AtmM    ("_⇧^m'(_,_')")
    and PrdM    ("_⇧^m'(_')")
    and NegM    ("¬⇧^m _" [58] 59)
    and AndM    (infixr "∧⇧^m" 56)
    and ExM     (binder "∃⇧^m" 53)
    and ExM2    (binder "∃⇧^m⇩₂" 53)
    and OrM     (infixr "∨⇧^m" 54)
    and ImpM    (infixr "⊃⇧^m" 55)
    and IffM    (infixr "⟷⇧^m" 54)
    and AllM    (binder "∀⇧^m" 53)
    and AllM2   (binder "∀⇧^m⇩₂" 53)
    and ValM    ("⊨⇧^m _" 9)
    and DpToShM ("⦇_⦈")

end