module Everything where
import Common
import Common.Context
import Common.ContextPair
import Common.Predicate
import Common.PredicateBasedContext
import Common.Semantics
import Common.UntypedContext
import BasicIPC.Syntax.Common
import BasicIPC.Syntax.ClosedHilbertSequential
import BasicIPC.Syntax.ClosedHilbert
import BasicIPC.Syntax.HilbertSequential
import BasicIPC.Syntax.Hilbert
import BasicIPC.Syntax.Gentzen
import BasicIPC.Syntax.GentzenNormalForm
import BasicIPC.Syntax.GentzenSpinalNormalForm
import BasicIPC.Syntax.Translation
import BasicIPC.Semantics.BasicTarski
import BasicIPC.Semantics.TarskiGluedClosedImplicit
import BasicIPC.Semantics.TarskiGluedClosedHilbert
import BasicIPC.Semantics.TarskiConcreteGluedImplicit
import BasicIPC.Semantics.TarskiConcreteGluedHilbert
import BasicIPC.Semantics.TarskiConcreteGluedGentzen
import BasicIPC.Semantics.KripkeConcreteGluedImplicit
import BasicIPC.Semantics.KripkeConcreteGluedHilbert
import BasicIPC.Semantics.KripkeConcreteGluedGentzen
import BasicIPC.Semantics.KripkeConcrete
import BasicIPC.Semantics.KripkeMcKinseyTarski
import BasicIPC.Semantics.KripkeGodel
import BasicIPC.Metatheory.ClosedHilbert-BasicTarski
import BasicIPC.Metatheory.ClosedHilbert-TarskiGluedClosedImplicit
import BasicIPC.Metatheory.ClosedHilbert-TarskiGluedClosedHilbert
import BasicIPC.Metatheory.Hilbert-BasicTarski
import BasicIPC.Metatheory.Hilbert-TarskiGluedClosedImplicit
import BasicIPC.Metatheory.Hilbert-TarskiGluedClosedHilbert
import BasicIPC.Metatheory.Hilbert-TarskiConcreteGluedImplicit
import BasicIPC.Metatheory.Hilbert-TarskiConcreteGluedHilbert
import BasicIPC.Metatheory.Hilbert-TarskiConcreteGluedGentzen
import BasicIPC.Metatheory.Hilbert-KripkeConcreteGluedImplicit
import BasicIPC.Metatheory.Hilbert-KripkeConcreteGluedHilbert
import BasicIPC.Metatheory.Hilbert-KripkeConcreteGluedGentzen
import BasicIPC.Metatheory.Hilbert-KripkeConcrete
import BasicIPC.Metatheory.Hilbert-KripkeMcKinseyTarski
import BasicIPC.Metatheory.Hilbert-KripkeGodel
import BasicIPC.Metatheory.Gentzen-BasicTarski
import BasicIPC.Metatheory.Gentzen-TarskiGluedClosedImplicit
import BasicIPC.Metatheory.Gentzen-TarskiConcreteGluedImplicit
import BasicIPC.Metatheory.Gentzen-TarskiConcreteGluedHilbert
import BasicIPC.Metatheory.Gentzen-TarskiConcreteGluedGentzen
import BasicIPC.Metatheory.Gentzen-KripkeConcreteGluedImplicit
import BasicIPC.Metatheory.Gentzen-KripkeConcreteGluedHilbert
import BasicIPC.Metatheory.Gentzen-KripkeConcreteGluedGentzen
import BasicIPC.Metatheory.Gentzen-KripkeConcrete
import BasicIPC.Metatheory.Gentzen-KripkeMcKinseyTarski
import BasicIPC.Metatheory.Gentzen-KripkeGodel
import BasicIPC.Metatheory.GentzenNormalForm-KripkeConcrete
import BasicIPC.Metatheory.GentzenNormalForm-KripkeMcKinseyTarski
import BasicIPC.Metatheory.GentzenNormalForm-KripkeGodel
import BasicIPC.Metatheory.GentzenSpinalNormalForm-HereditarySubstitution
import BasicT.Syntax.Common
import BasicT.Syntax.Gentzen
import BasicT.Syntax.GentzenNormalForm
import BasicT.Semantics.BasicTarski
import BasicT.Metatheory.Gentzen-BasicTarski
import BasicT.Metatheory.GentzenNormalForm-Unknown
import IPC.Syntax.Common
import IPC.Syntax.ClosedHilbertSequential
import IPC.Syntax.ClosedHilbert
import IPC.Syntax.HilbertSequential
import IPC.Syntax.Hilbert
import IPC.Syntax.Gentzen
import IPC.Syntax.GentzenNormalForm
import IPC.Syntax.GentzenSpinalNormalForm
import IPC.Syntax.Translation
import IPC.Semantics.BasicTarski
import IPC.Semantics.KripkeExploding
import IPC.Metatheory.ClosedHilbert-BasicTarski
import IPC.Metatheory.Hilbert-BasicTarski
import IPC.Metatheory.Gentzen-BasicTarski
import IPC.Metatheory.Gentzen-KripkeExploding
import IPC.Metatheory.GentzenNormalForm-KripkeExploding
import IPC.Metatheory.GentzenSpinalNormalForm-HereditarySubstitution
import BasicIS4.Syntax.Common
import BasicIS4.Syntax.ClosedHilbertSequential
import BasicIS4.Syntax.ClosedHilbert
import BasicIS4.Syntax.HilbertSequential
import BasicIS4.Syntax.Hilbert
import BasicIS4.Syntax.Gentzen
import BasicIS4.Syntax.DyadicHilbertSequential
import BasicIS4.Syntax.DyadicHilbert
import BasicIS4.Syntax.DyadicGentzen
import BasicIS4.Syntax.DyadicGentzenNormalForm
import BasicIS4.Syntax.DyadicGentzenSpinalNormalForm
import BasicIS4.Syntax.LabelledGentzen
import BasicIS4.Syntax.Translation
import BasicIS4.Semantics.BasicKripkeOno
import BasicIS4.Semantics.BasicKripkeBozicDosen
import BasicIS4.Semantics.BasicKripkeEwald
import BasicIS4.Semantics.BasicKripkeAlechina
import BasicIS4.Semantics.TarskiClosedOvergluedImplicit
import BasicIS4.Semantics.TarskiClosedOvergluedHilbert
import BasicIS4.Semantics.TarskiOvergluedImplicit
import BasicIS4.Semantics.TarskiOvergluedHilbert
import BasicIS4.Semantics.TarskiOvergluedGentzen
import BasicIS4.Semantics.TarskiGluedImplicit
import BasicIS4.Semantics.TarskiGluedHilbert
import BasicIS4.Semantics.TarskiGluedGentzen
import BasicIS4.Semantics.TarskiOvergluedDyadicImplicit
import BasicIS4.Semantics.TarskiOvergluedDyadicHilbert
import BasicIS4.Semantics.TarskiOvergluedDyadicGentzen
import BasicIS4.Semantics.TarskiGluedDyadicImplicit
import BasicIS4.Semantics.TarskiGluedDyadicHilbert
import BasicIS4.Semantics.TarskiGluedDyadicGentzen
import BasicIS4.Equipment.KripkeCanonical
import BasicIS4.Equipment.KripkeNonCanonical
import BasicIS4.Equipment.KripkeDyadicCanonical
import BasicIS4.Equipment.KripkeDyadicNonCanonical
import BasicIS4.Metatheory.ClosedHilbert-TarskiClosedOvergluedImplicit
import BasicIS4.Metatheory.ClosedHilbert-TarskiClosedOvergluedHilbert
import BasicIS4.Metatheory.Hilbert-BasicKripkeOno
import BasicIS4.Metatheory.Hilbert-BasicKripkeBozicDosen
import BasicIS4.Metatheory.Hilbert-BasicKripkeEwald
import BasicIS4.Metatheory.Hilbert-BasicKripkeAlechina
import BasicIS4.Metatheory.Hilbert-TarskiClosedOvergluedImplicit
import BasicIS4.Metatheory.Hilbert-TarskiClosedOvergluedHilbert
import BasicIS4.Metatheory.Hilbert-TarskiOvergluedImplicit
import BasicIS4.Metatheory.Hilbert-TarskiOvergluedHilbert
import BasicIS4.Metatheory.Hilbert-TarskiOvergluedGentzen
import BasicIS4.Metatheory.Hilbert-TarskiGluedImplicit
import BasicIS4.Metatheory.Hilbert-TarskiGluedHilbert
import BasicIS4.Metatheory.Gentzen-BasicKripkeOno
import BasicIS4.Metatheory.Gentzen-BasicKripkeBozicDosen
import BasicIS4.Metatheory.Gentzen-BasicKripkeEwald
import BasicIS4.Metatheory.Gentzen-BasicKripkeAlechina
import BasicIS4.Metatheory.Gentzen-TarskiClosedOvergluedImplicit
import BasicIS4.Metatheory.Gentzen-TarskiOvergluedImplicit
import BasicIS4.Metatheory.Gentzen-TarskiOvergluedGentzen
import BasicIS4.Metatheory.Gentzen-TarskiGluedImplicit
import BasicIS4.Metatheory.Gentzen-TarskiGluedGentzen
import BasicIS4.Metatheory.DyadicHilbert-BasicKripkeOno
import BasicIS4.Metatheory.DyadicHilbert-BasicKripkeBozicDosen
import BasicIS4.Metatheory.DyadicHilbert-BasicKripkeEwald
import BasicIS4.Metatheory.DyadicHilbert-BasicKripkeAlechina
import BasicIS4.Metatheory.DyadicHilbert-TarskiOvergluedDyadicImplicit
import BasicIS4.Metatheory.DyadicHilbert-TarskiOvergluedDyadicHilbert
import BasicIS4.Metatheory.DyadicHilbert-TarskiOvergluedDyadicGentzen
import BasicIS4.Metatheory.DyadicHilbert-TarskiGluedDyadicImplicit
import BasicIS4.Metatheory.DyadicHilbert-TarskiGluedDyadicHilbert
import BasicIS4.Metatheory.DyadicGentzen-BasicKripkeOno
import BasicIS4.Metatheory.DyadicGentzen-BasicKripkeBozicDosen
import BasicIS4.Metatheory.DyadicGentzen-BasicKripkeEwald
import BasicIS4.Metatheory.DyadicGentzen-BasicKripkeAlechina
import BasicIS4.Metatheory.DyadicGentzen-TarskiOvergluedDyadicImplicit
import BasicIS4.Metatheory.DyadicGentzen-TarskiOvergluedDyadicGentzen
import BasicIS4.Metatheory.DyadicGentzen-TarskiGluedDyadicImplicit
import BasicIS4.Metatheory.DyadicGentzen-TarskiGluedDyadicGentzen
import BasicIS4.Metatheory.DyadicGentzenSpinalNormalForm-HereditarySubstitution
import BasicICML.Syntax.Common
import BasicICML.Syntax.DyadicGentzen
import BasicICML.Syntax.DyadicGentzenNormalForm
import BasicICML.Syntax.DyadicGentzenSpinalNormalForm
import BasicICML.Metatheory.DyadicGentzenSpinalNormalForm-HereditarySubstitution
import BasicILP.Syntax.Common
import BasicILP.Syntax.DyadicGentzen
import OldBasicILP.UntypedSyntax.Common
import OldBasicILP.UntypedSyntax.ClosedHilbertSequential
import OldBasicILP.UntypedSyntax.ClosedHilbert
import OldBasicILP.UntypedSyntax.Translation
import OldBasicILP.Syntax.Common
import OldBasicILP.Syntax.ClosedHilbertSequential
import OldBasicILP.Syntax.ClosedHilbert
import OldBasicILP.Syntax.Translation
import OlderBasicILP.Indirect
import OlderBasicILP.Indirect.Hilbert.Sequential
import OlderBasicILP.Indirect.Hilbert.Nested
import OlderBasicILP.Indirect.Gentzen
import OlderBasicILP.Direct.Hilbert.Nested
import OlderBasicILP.Direct.Gentzen