namespace http://cds.omdoc.org/examples ❚

import lfx http://gl.mathhub.info/MMT/LFX/TypedHierarchy ❚
import finite http://gl.mathhub.info/MMT/LFX/Finite ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚
import ur http://cds.omdoc.org/urtheories ❚

rule scala://parser.api.mmt.kwarc.info?MMTURILexer❚

theory LFXI = 
  include ☞ur:?DHOL❙
  include ☞lfx:?LFHierarchy❙
  rule rules?InductiveTypes❙
  rule rules?InductiveDefinitions❙
  rule rules?InductiveMatch❙
  rule rules?InductiveProofDefinitions❙
  rule rules?Reflections❙

  rule rules?Records❙
  rule rules?RecordDefinitions❙
❚