From: Andrea Asperti Date: Tue, 20 Feb 2001 10:30:36 +0000 (+0000) Subject: New stylesheets from content to html. X-Git-Tag: v0_1_2~108 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f5a06d5c51c59dcfe432a3b4236f0a4189f031f6;p=helm.git New stylesheets from content to html. -- andrea --- diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index 5b57eb0ff..62a4936f0 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -32,6 +32,12 @@ + + + +

getciconly?uri=

+ +

/apply?key=C1&key=HC2&param.getterURL=&param.processorURL=&xmluri=

@@ -44,15 +50,20 @@ - + + - - + + + +

@@ -67,7 +78,7 @@ - +

@@ -75,7 +86,6 @@ -

@@ -100,8 +110,173 @@

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + " + + : + + . + + + + Õ + + : + + . + + + + + ( + + + ® + + + ) + + + + ( + + + + + + ) + + + + ( + + :> + + ) + + + Prop + + + Set + + + Type + + + + < + + > + CASE + + OF + + + + | + + + + Þ + + + + + + FIX + + { + + + : + + := + + + + } + + + ; + + + + + + + COFIX + + { + + + : + + := + + + + } + + + ; + + + + + + + we proved + + + + + + + l + + : + + . + + + + + + + @@ -114,17 +289,19 @@ - + + - P + " :

+ +

@@ -134,16 +311,35 @@ - - P - - : - - . - + + + + + + Õ + + : + + +
+ + + + . + + + + + + + + + + @@ -151,27 +347,25 @@

-
+

- ® + + ® +

) - ( - - - ® - - ) + + @@ -180,7 +374,7 @@

-
+

@@ -191,13 +385,7 @@ )

- ( - - - - - - ) + @@ -209,7 +397,7 @@ (

:> @@ -219,11 +407,7 @@ ) - ( - - :> - - ) + @@ -257,7 +441,7 @@ OF

-
+

@@ -270,34 +454,18 @@ - Þ + Þ

- < - - > - CASE - - OF - - - - | - - - - Þ - - - - + + @@ -305,7 +473,7 @@ { -
+

@@ -315,7 +483,7 @@ -
+

@@ -324,41 +492,25 @@ -
+

} - FIX - - { - - - : - - := - - - - } - - - ; - - - + + COFIX

{ -
+

@@ -369,7 +521,7 @@ -
+

@@ -379,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 +
+ + + + ( + + ) + + + +
+ + + + + + + + @@ -420,16 +770,17 @@ + - l + l

@@ -439,13 +790,7 @@ - - l - - : - - . - + @@ -454,11 +799,6 @@ - -

@@ -532,15 +872,15 @@

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

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

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

-UNFINISHED PROOF ()
+UNFINISHED PROOF ()
THESIS: -
+
CONJECTURES: -
+
@@ -582,7 +926,7 @@ CONJECTURES: -
+
PROOF: @@ -620,14 +964,14 @@ PROOF: - ]
+ ]
OF ARITY -
+
BUILT FROM: -
+
@@ -654,7 +998,7 @@ PROOF:

-VARIABLE
+VARIABLE
TYPE = diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl index bb6bea3ba..f52525ebf 100644 --- a/helm/style/html_init.xsl +++ b/helm/style/html_init.xsl @@ -32,6 +32,128 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + + + + + ) + + + + + + + + + + + + + + + - + + + + + ( + + + + + + - + + + ) + + + + + + + + + + + + + + + Ø + + + + + + + + + + + + + + + $ + + + : + + . + + + + + - - - - - - - - - - ) + @@ -164,16 +275,7 @@ ) - ( - - - - - - - - - - ) + @@ -232,19 +334,7 @@ - - - - - $ - - - : - - . - - - + diff --git a/helm/style/html_reals.xsl b/helm/style/html_reals.xsl index de3196b12..2b4ca35e5 100644 --- a/helm/style/html_reals.xsl +++ b/helm/style/html_reals.xsl @@ -32,8 +32,128 @@ + + + + + + + + + + + + + + lim + + _{+
+ ®
+
+} + + + + + + + + + + + + + + ^d + / + _{+ d
+
+} + + + + + + + + + + | + + | + + + + + + + + + + ! + + + + + + + + + (sqr + + ) + + + + + + + + + + ^{+
+} + + + + + + + + + + + + + + + + + + + + + + + + + { + + , + + } + + + + + + + @@ -65,26 +185,12 @@ - - - - - lim - - _{-
- ®
-
-} - - - + - @@ -107,6 +213,7 @@ + @@ -208,17 +315,7 @@ } - - - - - - - { - - , - - } + diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl index 78f4a5b9e..97e3b1e07 100644 --- a/helm/style/html_set.xsl +++ b/helm/style/html_set.xsl @@ -32,63 +32,143 @@ - + + + - + + + + + + + + + Æ + + + + + { + + : + + | + + } + + + { + + + + + } + + + , + + + + + + + + + + + + - + - - + | + + | + + + + + - - - ( - - - -
- - - - - - - - Î - - - - - ) + + + + + + + + + + + + + + + + + + + + + + - - ( - - - - - - Î - - - ) - + + ( + + + + + + + + + + + ) - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -100,22 +180,26 @@ - Ï + + + + + + + + ) - ( - - Ï - - ) + + @@ -133,9 +217,9 @@ - + - + { : @@ -153,19 +237,6 @@ } - { - - : - - | - - } - - - - - - { @@ -180,263 +251,17 @@ - } - - - { - - - - - } - - - , - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - -
- - - - - - - - Ç - - - - - ) - - - ( - - - - - - Ç - - - ) - - - - - - - - - - - - - - - - - - ( - - - -
- - - - - - - - È - - - - - ) - - - ( - - - - - - È - - - ) - - - - - - - - - - - - - - - - - ( - - - -
- - - - - - - - Í - - - - - ) - - - ( - - - - - - Í - - - ) - - - - - - - - - - - - - - - - - ( - - - -
- - - - - - - - Ì - - - - - ) - - - ( - - - - - - Ì - - - ) - - - - - - - - - - - - - - - - - - - ( - - - -
- - - - - - - - / - - - - - ) - - - ( - - - - - - / - - - ) - - - + } + + + + + + + + + + diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 86675e553..900dd4bf6 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -1045,6 +1045,7 @@ +