X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=62a4936f0c071e83f6b74fa5da0061a2769a39c3;hb=f5a06d5c51c59dcfe432a3b4236f0a4189f031f6;hp=d3cb774084c37549047d25088ed2929e7fb570c0;hpb=8e1a7e55cbc7750446f0a7ab3d071190594243fb;p=helm.git diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index d3cb77408..62a4936f0 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -32,15 +32,17 @@ + + + +getciconly?uri= + +/apply?key=C1&key=HC2&param.getterURL=&param.processorURL=&xmluri= - - - - @@ -48,15 +50,20 @@ - + + - - + + + + @@ -71,7 +78,7 @@ -   +   @@ -79,7 +86,6 @@ - @@ -104,8 +110,173 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + " + + : + + . + + + + Õ + + : + + . + + + + + ( + + + ® + + + ) + + + + ( + + +   + + + ) + + + + ( + + :> + + ) + + + Prop + + + Set + + + Type + + + + < + + > + CASE + + OF + + + + | + + + + Þ + + + + + + FIX + + { + + + : + + := + + + + } + + + ; + + + + + + + COFIX + + { + + + : + + := + + + + } + + + ; + + + + + + + we proved + + + + + + + l + + : + + . + + + + + + + @@ -118,17 +289,43 @@ - + + - P + " + + : + + + +
+ + + + . + + + + + + + + + + + + + + Õ : -
+
@@ -138,16 +335,11 @@ - - P - - : - - . - + + @@ -155,27 +347,25 @@ -
+
- ® + + ® + ) - ( - - - ® - - ) + + @@ -184,7 +374,7 @@ -
+
@@ -195,13 +385,7 @@ ) - ( - - -   - - - ) + @@ -213,7 +397,7 @@ ( -
+
:> @@ -223,11 +407,7 @@ ) - ( - - :> - - ) + @@ -261,7 +441,7 @@ OF -
+
@@ -274,34 +454,18 @@ - Þ + Þ - < - - > - CASE - - OF - - - - | - - - - Þ - - - - + + @@ -309,7 +473,7 @@ { -
+
@@ -319,7 +483,7 @@ -
+
@@ -328,41 +492,25 @@ -
+
} - FIX - - { - - - : - - := - - - - } - - - ; - - - + + COFIX { -
+
@@ -373,7 +521,7 @@ -
+
@@ -383,36 +531,234 @@ -
+
} - COFIX - - { - - - : - - := - - - - } - - - ; - - - + - - + + + + + + + + +
+ + + + + we proved  + + + + + + + + + +
+ + + + + + + + + + + + + +
+ + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + Consider  + + + +
+ + + + Rewrite  + +  with  + +  by  + + + + + + + +
+ + + + Then apply it to  + + + + + + + + + + + + Consider  + + + +
+ + + + In particular, we have +
+ + + + ( + + )  + + + +
+ + + + ( + + )  + + + +
+ + + + + + + + + + + + + + + + + Consider  + + + +
+ + + + We prove  + +  by cases: +
+ + + + * + + + +
+ + + + * + + + + + + + + + + + + + + Consider  + + + + + +
+ + + + Let  + + : + +  such that +
+ + + + ( + + ) + + + +
+ + + + + + + + @@ -424,16 +770,17 @@ + - l + l : -
+
@@ -443,13 +790,7 @@ - - l - - : - - . - + @@ -458,11 +799,6 @@ - - @@ -536,15 +872,15 @@

-DEFINITION ()
-TYPE =
+DEFINITION ()
+TYPE =
-
-BODY =
+
+BODY =
@@ -559,8 +895,12 @@ BODY =

-AXIOM ()
-TYPE = +AXIOM ()
+TYPE =
+ + + +

@@ -571,13 +911,13 @@ TYPE =

-UNFINISHED PROOF ()
+UNFINISHED PROOF ()
THESIS: -
+
CONJECTURES: -
+
@@ -586,7 +926,7 @@ CONJECTURES: -
+
PROOF: @@ -624,14 +964,14 @@ PROOF: - ]
+ ]
OF ARITY -
+
BUILT FROM: -
+
@@ -658,7 +998,7 @@ PROOF:

-VARIABLE
+VARIABLE
TYPE =