<!-- A DTD for XML instantiations of the SCL -->
<!-- Chris Menzel, 24 Jul 2003 -->

<!--"theory" is taken as the root element, as the DTD can then be applied to 
sets of formulas.-->

š{!ELEMENT formula (and | or | implies | iff | not | forall | exists | atom)š}

š{!ELEMENT and (formula*)š}

š{!ELEMENT or (formula*)š}

š{!ELEMENT implies (formula, formula)š}

š{!ELEMENT iff (formula, formula)š}

š{!ELEMENT not (formula)š}

š{!ELEMENT forall (varlist, formula)š}

š{!ELEMENT exists (varlist, formula)š}

š{!ELEMENT varlist (genvar | sortvar)+š}

š{!ELEMENT sortvar (genvar, predcon)š}

š{!ELEMENT atom (pred, (indcon | genvar | fnterm)*, seqvar{0,1})š}

š{!ELEMENT fnterm (fnsym, (indcon | genvar | fnterm)*, seqvar{0,1})š}

š{!ELEMENT pred (predcon | genvar) (#PCDATA)š}

š{!ELEMENT indcon (#PCDATA)š}

š{!ELEMENT predcon (#PCDATA)š}

š{!ELEMENT fnsym (#PCDATA)š}

š{!ELEMENT genvar (#PCDATA)š}

š{!ELEMENT seqvar (#PCDATA)š}