X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=856fd69718a66103a38e43811ee1b836de23fc0c;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=1211e4881be96e555eba8e9d9245832cff02fdb8;hpb=19681f7b0c71fbb8c9e3442c0880533731094046;p=helm.git diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index 1211e4881..856fd6971 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -59,7 +59,7 @@ media-type="text/html" doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" /> - + @@ -167,8 +167,32 @@ <xsl:value-of select="$CICURI"/> + + + if(document.getElementById) + for(var i=0;i<document.to_be_deleted.length;i++) + Hide(document.getElementById(document.to_be_deleted[i])); + @@ -322,14 +346,14 @@ CASE OF - + | - + @@ -383,11 +407,19 @@ - - + +  proves  + +  which is equivalent to  + + + + + + letin1 (inline error) @@ -900,7 +932,7 @@ OF - +
@@ -1048,19 +1080,177 @@ - - - -
- - - - - we proved  + + + + + + + + +   + + + +
+ + + + we proved  +
+ + + +
+ + + + + + + + + + + +   + + + + + + + + + + + We have the following equality chain: + + +
+ + + + + + + + +  = + + + + + + + + + +
+ + + + + + +
+
+
+ + + We have the following chain of disequalities: + + +
+ + + + + + + + +   + + + + +   + + + + + + +
+ + + + + + +
+
+
@@ -1112,20 +1302,22 @@ - + - + - + + select="($charlength_first + $charlength_second) > $framewidth"/> + select="($charlength_second + $charlength_side_proof) > $framewidth"/> - + + +
@@ -1804,7 +1996,27 @@
- + + + + + + + + + + + + + + + + + + + + + @@ -1913,8 +2125,43 @@ CONJECTURES: - : - + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ :? _ + + + + |- : + @@ -1994,6 +2241,12 @@ VARIABLE
TYPE = + +
+BODY = + + +