MODULE (
  HEADER (
    SPEC (
      NAME ("subst"),
      VERSION ("1.00.00"),
      VERSION ("1.01.00"),
      LOCATIONS (
        LOCATION (".")
      )
    ),
    HEADLINE ("Substitution of Proof Lines"),
    DESCRIPTION (
      "This module declares the general rule for substituting variables."
    ),
    EMAIL ("principa@meyling.com"),
    AUTHORS (
      AUTHOR ("Michael Meyling",EMAIL ("michael@meyling.com"))
    )
  ),
  IMPORTS (
    IMPORT (
      SPEC (
        NAME ("propaxiom"),
        VERSION ("1.00.00"),
        VERSION ("1.00.00"),
        LOCATIONS (
          LOCATION (".")
        )
      )
    ),
    IMPORT (
      SPEC (
        NAME ("predaxiom"),
        VERSION ("1.00.00"),
        VERSION ("1.00.00"),
        LOCATIONS (
          LOCATION (".")
        )
      )
    )
  ),
  USEDBY (
    SPEC (
      NAME ("prophilbert1"),
      VERSION ("1.00.00"),
      VERSION ("1.02.00"),
      LOCATIONS (
        LOCATION (".")
      )
    )
  ),
  PARAGRAPHS (
    PARAGRAPH (
      LABEL ("rule8"),
      "If a proof line could be derived by using <a href=""propaxiom_1.00.00_1.00.00.html#rule4"">rename proposition variable</a>, <a href=""predaxiom_1.00.00_1.00.00.html#predrule1"">rename bound subject variable</a> and <a href=""predaxiom_1.00.00_1.00.00.html#predrule2"">rename free subject variable</a> multiple times, we declare a new rule to shorten that derivation:",
      DECLARERULE (
        "SUBSTLINE",
        "Substitute Variables"
      ),
      "The use of this rule could always be replaced by proof lines that make only use of the referenced rules."
    )
  )
)