X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=1a66b86dd489cf8280e0d4a870afcf4abdec3717;hb=7ff85e55518d06d96b9abbea4aa68d83e6be35b0;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..1a66b86dd 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" /> - + @@ -69,6 +69,12 @@ + + + + + + @@ -114,6 +120,12 @@ + + + + + + @@ -167,8 +179,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])); + @@ -191,6 +227,12 @@ +   @@ -248,6 +290,7 @@ + @@ -286,6 +329,30 @@ ) + + + ( + + + + + + + + ) + + + + ( + + + + + + + + ) + ( @@ -300,7 +367,7 @@ ( - :> + : ) @@ -321,7 +388,8 @@ CASE OF - + + | @@ -337,6 +405,23 @@ select="./*[1]"/> + + + + { + + + / + + + + + + + + } + + FIX @@ -381,11 +466,28 @@ - - + + + if + + then + + else + + + +  proves  + +  which is equivalent to  + + + + + + letin1 (inline error) @@ -415,13 +517,24 @@ [ - - - - - - - + + + + + + + + + + + + + + + + + + ] @@ -430,13 +543,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -446,13 +570,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -464,87 +599,175 @@ - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - * - - + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + * + + + - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - * - - + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + * + + + - | + + + | + + + | + + - | + + + | + + + | + + @@ -552,13 +775,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -600,7 +834,12 @@ + + + + + @@ -687,6 +926,62 @@ + + + + + ( + + + +
+ + + + + + + + + + + + + ) +
+ + + +
+
+ + + + + ( + + + +
+ + + + + + + + + + + + + ) +
+ + + +
+
@@ -765,7 +1060,8 @@ OF - + +
@@ -778,14 +1074,15 @@ |
- + - + @@ -794,14 +1091,14 @@ - + - @@ -905,25 +1202,224 @@
+ + + if + + + +
+ + + + then + + + +
+ + + + else + + + +
- - - -
- - - - - we proved  - + + + + + + + + +   + +
+ + + + we proved  + + + +
+ + + + and by delta equivalence + + + +
+
+ + +
+ + + + we proved  +
+ + + +
+
+ + + + + + + + + + + +   + + + + + + + + + + + We have the following equality chain: + + +
+ + + + + + + + +  = + + + + + + + + + +
+ + + + + + +
+
+
+ + + We have the following chain of disequalities: + + +
+ + + + + + + + +   + + + + +   + + + + + + +
+ + + + + + +
+
+
@@ -975,20 +1471,22 @@
- + - + - + + select="($charlength_first + $charlength_second) > $framewidth"/> + select="($charlength_second + $charlength_side_proof) > $framewidth"/> - + + +
@@ -1326,13 +1824,24 @@ [ - - - - - - - + + + + + + + + + + + + + + + + + + ] @@ -1341,13 +1850,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -1357,13 +1877,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -1375,87 +1906,175 @@ - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - * - - + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + * + + + - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - * - - + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + * + + + - | + + + | + + + | + + - | + + + | + + + | + + @@ -1463,13 +2082,24 @@ - - - - - - - + + + + + + + + + + + + + + + + + + @@ -1535,7 +2165,27 @@ - + + + + + + + + + + + + + + + + + + + + + @@ -1644,8 +2294,43 @@ CONJECTURES: - : - + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ :? _ + + + + |- : + @@ -1725,6 +2410,12 @@ VARIABLE
TYPE = + +
+BODY = + + +