From 3aa2fd56797217a73b59e25bbe961dbc8c08bb2f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 5 Nov 2001 09:06:40 +0000 Subject: [PATCH] Algebra notation. --- helm/style/algebra.xsl | 453 +++++++++++++++++++++++++++++++++ helm/style/content_to_html.xsl | 88 ++++++- helm/style/drop_coercions.xsl | 35 +++ helm/style/headercontent.xsl | 1 + helm/style/html_init.xsl | 26 +- helm/style/html_reals.xsl | 65 ++++- helm/style/proofs.xsl | 64 ++++- helm/style/set.xsl | 47 ++++ 8 files changed, 771 insertions(+), 8 deletions(-) create mode 100644 helm/style/algebra.xsl diff --git a/helm/style/algebra.xsl b/helm/style/algebra.xsl new file mode 100644 index 000000000..81eed377a --- /dev/null +++ b/helm/style/algebra.xsl @@ -0,0 +1,453 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + + + + app + + $x + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + + + $x + + + + + app + + $x + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + + + + + + + app + + $x + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index 6e7ff7ca5..a9cc91a96 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" /> - + @@ -408,11 +408,14 @@ - +  proves  + + letin1 (inline error) + @@ -1126,6 +1129,87 @@ + + + + + + + + + + + +   + + + + + + + + + + + We have the following equality chain: + + +
+ + + + + + + + +  = + + + + + + + + + +
+ + + + + + +
+
+
diff --git a/helm/style/drop_coercions.xsl b/helm/style/drop_coercions.xsl index 9731d6601..f2bc44d0d 100644 --- a/helm/style/drop_coercions.xsl +++ b/helm/style/drop_coercions.xsl @@ -118,6 +118,41 @@
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/headercontent.xsl b/helm/style/headercontent.xsl index a46023db5..f60883079 100644 --- a/helm/style/headercontent.xsl +++ b/helm/style/headercontent.xsl @@ -37,6 +37,7 @@ + diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl index 06e23deca..d3c9d1992 100644 --- a/helm/style/html_init.xsl +++ b/helm/style/html_init.xsl @@ -62,6 +62,9 @@ + + + @@ -114,6 +117,9 @@ + + + @@ -143,8 +149,24 @@ + + + + + + + + + + + + + + + + + |m:geq|m:gt|m:plus|m:times|m:divide]"> ( @@ -262,7 +284,7 @@ + |m:geq|m:gt|m:plus|m:times|m:divide]"> diff --git a/helm/style/html_reals.xsl b/helm/style/html_reals.xsl index 15071579a..a78f454bd 100644 --- a/helm/style/html_reals.xsl +++ b/helm/style/html_reals.xsl @@ -41,6 +41,9 @@ + + + ??? @@ -56,6 +59,9 @@ + + + ??? @@ -72,6 +78,58 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -202,6 +260,9 @@ + + + @@ -384,8 +445,8 @@ - + diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl index 0651f65ec..4c207e482 100644 --- a/helm/style/proofs.xsl +++ b/helm/style/proofs.xsl @@ -79,7 +79,10 @@ - + + @@ -152,12 +155,55 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + eq_chain + + + + + + + + diff --git a/helm/style/set.xsl b/helm/style/set.xsl index 5ff4fce0b..f1f7b7e50 100644 --- a/helm/style/set.xsl +++ b/helm/style/set.xsl @@ -488,4 +488,51 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensemble + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + + + + + app + + $x + + + + + + + + + + + + + -- 2.39.2