+ <xsl:copy-of select="document(concat($interfaceURL,@src,'_xml'))" />
+</xsl:template>
+
+<xsl:template match="subst:proofcheckerURL">
+ <xsl:value-of select="$proofcheckerURL"/>
+</xsl:template>
+
+<xsl:template match="subst:interfaceURL">
+ <xsl:value-of select="$interfaceURL"/>
+</xsl:template>
+
+<xsl:template match="subst:processorURL">
+ <xsl:value-of select="$processorURL"/>
+</xsl:template>
+
+<xsl:template match="subst:getterURL">
+ <xsl:value-of select="$getterURL"/>
+</xsl:template>
+
+<xsl:template match="subst:draw_graphURL">
+ <xsl:value-of select="$draw_graphURL"/>
+</xsl:template>
+
+<xsl:template match="subst:profile">
+ <xsl:value-of select="$profile"/>
+</xsl:template>
+
+<xsl:template match="subst:url">
+ <xsl:value-of select="$url"/>
+</xsl:template>
+
+<xsl:template match="subst:CICURI">
+ <xsl:value-of select="$CICURI"/>
+</xsl:template>
+
+<xsl:template match="subst:base_CICURI">
+ <xsl:variable name="len" select="string-length($CICURI)" />
+ <xsl:variable name="extension">
+ <xsl:choose>
+ <xsl:when test="substring($CICURI,$len)='/'">#</xsl:when>
+ <xsl:when test="substring($CICURI,$len - 6)='.theory'">.theory</xsl:when>
+ <xsl:when test="substring($CICURI,$len - 3)='.con'">.con</xsl:when>
+ <xsl:when test="substring($CICURI,$len - 3)='.ind'">.ind</xsl:when>
+ <xsl:when test="substring($CICURI,$len - 3)='.var'">.var</xsl:when>
+ <xsl:when test="substring($CICURI,$len - 8)='.con.body'">.con.body</xsl:when>
+ <xsl:otherwise>
+<!--
+ <xsl:message terminate="no">
+ resolve_topurl.xsl: assertion failed
+ </xsl:message>
+-->
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+ <xsl:call-template name="name_of_uri">
+ <xsl:with-param name="uri">
+ <xsl:choose>
+ <xsl:when test="substring($CICURI,$len)='/'">
+ <xsl:value-of select="concat(substring($CICURI,1,$len - 1),'#')" />
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:value-of select="$CICURI" />
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:with-param>
+ <xsl:with-param name="extension" select="$extension" />
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="subst:annotations">
+ <xsl:value-of select="$annotations"/>
+</xsl:template>
+
+<xsl:template match="subst:makeURL">
+ <xsl:call-template name="makeURL">
+ <xsl:with-param name="uri" select="$CICURI"/>
+ <xsl:with-param name="createframeset" select="false()"/>
+ </xsl:call-template>