<xsl:value-of select="$CICURI"/>

X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=b5c7481bf9590eb4a20a5c491dd937621cad6b12;hb=5868bef6637af919fbb48a83c24268bb85bdef6a;hp=461dfddadaaab720a9564151317844588150150b;hpb=b564f0671c133928e372e352d972a7663b6a9136;p=helm.git diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index 461dfddad..b5c7481bf 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -29,16 +29,12 @@ - + - - - - -

getciconly?uri=

- -

/apply?keys=&param.naturalLanguage=&param.keys=&param.getterURL=&param.processorURL=&xmluri=

+ + + @@ -46,34 +42,171 @@ - - - - - - - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ??? + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ??? + + + + + + + + + - - - - - - - - - - + + + + + <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])); + + + + + + + + + + + + + + + @@ -123,12 +256,7 @@ - - - - - - +

@@ -144,10 +272,15 @@

- " + + + + +

@@ -155,7 +288,11 @@

- Õ + + + + +

@@ -166,9 +303,11 @@ (

- - ® - + + + + +

)

@@ -207,16 +346,21 @@ CASE

OF - + + | - - Þ + + + + + +

+ select="./*[1]"/>

@@ -264,34 +408,337 @@ - +

proves

+ + letin1 (inline error) + + + + + Contradiction. + From

we get - ( + ( - ) + ) and - ( + ( - ) + ) - ; + ; hence

+ + + + [ + + + + + + + + + + + + + + + + + + + + + ] + + + + _{+
+} + + + + + + + + + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + | + + + | + + + + + + | + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + [ + + ] + + - l + + + + +

@@ -314,13 +761,18 @@

- " + + + + +

@@ -345,7 +797,11 @@ - Õ + + + + +

@@ -378,9 +834,11 @@ - - ® - + + + + +

@@ -461,15 +919,19 @@

> +
+ + CASE

OF - + +

- +

@@ -479,11 +941,34 @@ | - - Þ - - - + + + + + + + + + + + +
+ + + + + + + + + + +

@@ -568,24 +1053,163 @@ - - - - - - - + + let + + := + +
-

- we proved + in + + + + + + + + + + + + + + + + + + + + + + +
+ + + + we proved + + + + +

+ + + + + + + + + + + + + + + + + + + + + + + We have the following equality chain: + + +
+ + + + + + + + + = + + + = + + + + + + +
+ + + + + + + + +

@@ -616,9 +1240,9 @@

- ( + ( - ) + )

@@ -636,16 +1260,49 @@

+ + + + + + + + + + + + + + +

Rewrite - - with - - by - + + + +
+ + + + + with + + + +
+ + + + + by + + + @@ -659,6 +1316,116 @@ Then apply it to

+ + + We prove + + + +
+ + + + by induction on + + + + + + + + + + + +
+ + + + Case + + + + +
+ + + + By induction hypothesis, we have: + +
+ + + + ( + + ) + + + + + +
+ + + + + + + + + + + + + + + + ( + + + + + : + + + ) + + + + + + + + +
+ + + + Contradiction. + @@ -681,9 +1448,9 @@

- ( + ( - ) + )

@@ -691,9 +1458,9 @@

- ( + ( - ) + )

@@ -705,6 +1472,62 @@ + + + + + + + + + + Consider + + + +
+ + + + We proceed by cases to prove + +
+ + + + Left: suppose + ( + + ) + +
+ + + + + + +
+ + + + Right: suppose + ( + + ) + +
+ + + + + + + @@ -729,7 +1552,7 @@

- * + Left:

@@ -737,7 +1560,7 @@

- * + Right:

@@ -763,16 +1586,16 @@ Let

- : + : such that

- ( + ( - ) + )

@@ -784,6 +1607,299 @@

+ + + + + + [ + + + + + + + + + + + + + + + + + + + + + ] + + + + _{+
+} + + + + + + + + + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + | + + + | + + + + + + | + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + [ + + ] + + @@ -800,7 +1916,11 @@ - l + + + + +

@@ -825,12 +1945,7 @@ - - - - - - +

@@ -840,7 +1955,27 @@ - + + + + + + + + + + + + + + + + + + + + + @@ -1030,6 +2165,12 @@ VARIABLE
TYPE =

+ +
+BODY = + + +