X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=856fd69718a66103a38e43811ee1b836de23fc0c;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=110732e912a07b60ffd18a77469e79665496decf;hpb=724c03286dd6d22091490ffdd8f66120c6c09dc8;p=helm.git diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index 110732e91..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])); + @@ -248,6 +272,7 @@ + @@ -321,7 +346,8 @@ CASE OF - + + | @@ -381,11 +407,19 @@ - - + +  proves  + +  which is equivalent to  + + + + + + letin1 (inline error) @@ -415,13 +449,24 @@ [ - - - - - - - + + + + + + + + + + + + + + + + + + ] @@ -430,13 +475,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -446,13 +502,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -464,87 +531,175 @@ - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - * - - + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + * + + + - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - * - - + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + * + + + - | + + + | + + + | + + - | + + + | + + + | + + @@ -552,13 +707,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -600,6 +766,7 @@ + @@ -765,7 +932,8 @@ OF - + +
@@ -778,14 +946,15 @@ |
- + - + @@ -794,14 +963,14 @@ - + - @@ -911,19 +1080,177 @@ - - - -
- - - - - we proved  + + + + + + + + +   + + + +
+ + + + we proved  +
+ + + +
+ + + + + + + + + + + +   + + + + + + + + + + + We have the following equality chain: + + +
+ + + + + + + + +  = + + + + + + + + + +
+ + + + + + +
+
+
+ + + We have the following chain of disequalities: + + +
+ + + + + + + + +   + + + + +   + + + + + + +
+ + + + + + +
+
+
@@ -975,20 +1302,22 @@ - + - + - + + select="($charlength_first + $charlength_second) > $framewidth"/> + select="($charlength_second + $charlength_side_proof) > $framewidth"/> - + + +
@@ -1326,13 +1655,24 @@ [ - - - - - - - + + + + + + + + + + + + + + + + + + ]
@@ -1341,13 +1681,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -1357,13 +1708,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -1375,87 +1737,175 @@ - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - * - - + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + * + + + - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - * - - + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + * + + + - | + + + | + + + | + + - | + + + | + + + | + + @@ -1463,13 +1913,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -1535,7 +1996,27 @@ - + + + + + + + + + + + + + + + + + + + + + @@ -1644,8 +2125,43 @@ CONJECTURES: - : - + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ :? _ + + + + |- : + @@ -1725,6 +2241,12 @@ VARIABLE
TYPE = + +
+BODY = + + +