Modified Files:

[helm.git] / helm / style / theory_pres.xsl
diff --git a/helm/style/theory_pres.xsl b/helm/style/theory_pres.xsl

index 5d60b9efafabab4fc77e85ab0153498123b8c184..b4a6e3cd8c864e742d28e6cacff91f19edc7555e 100644 (file)
--- a/helm/style/theory_pres.xsl
+++ b/helm/style/theory_pres.xsl
@@ -41,29 +41,31 @@
         doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN"
         doctype-system="DTD/xhtml1-transitional.dtd" />
  
-<xsl:template match="SECTION">
-<xsl:param name="subsect" select="0"/>
-    <xsl:choose>
-    <xsl:when test="$subsect = 0">
+<xsl:template match="Theory">
       <html> 
        <head></head>
        <body>
-       <h3>BEGIN SECTION</h3>
-       <xsl:apply-templates select="*"><xsl:with-param name="subsect" select="1"/></xsl:apply-templates>
-       <h3>END SECTION</h3>
+       <h2>THEORY<xsl:text>&#x00a0;</xsl:text><xsl:value-of select="@name"/></h2>
+       <xsl:apply-templates select="*"/>
+       <h2>END THEORY</h2>
        </body>
       </html>
-    </xsl:when>
-    <xsl:otherwise>
+</xsl:template>
+
+<xsl:template match="SECTION">
       <h3>BEGIN SECTION</h3>
-      <xsl:apply-templates select="*"><xsl:with-param name="subsect" select="1"/></xsl:apply-templates>
+     <xsl:apply-templates select="*"/>
       <h3>END SECTION</h3>
-    </xsl:otherwise>
-    </xsl:choose>
  </xsl:template>
  
-<xsl:template match="ENTITY">
-  <ENTITY uri="{@uri}"/>
+<xsl:template match="THEOREM|LEMMA|COROLLARY|FACT">
+     <h4><xsl:value-of select="name(.)"/><xsl:text>&#x00a0;</xsl:text><a href="{$uri}"><xsl:value-of select="@name"/></a></h4>
+    <ENTITY uri="{@uri}" type="1"/>
+</xsl:template>
+
+<xsl:template match="AXIOM|DEFINITION|VARIABLE">
+     <h4><xsl:value-of select="name(.)"/><xsl:text>&#x00a0;</xsl:text><a href="{$uri}"><xsl:value-of select="@name"/></a></h4>
+    <ENTITY uri="{@uri}" type="0"/>
  </xsl:template>
  
  </xsl:stylesheet>
@@ -73,3 +75,6 @@
  
  
  
+
+
+