From d88218090d8607c08455ad3f1791441c7b09f49a Mon Sep 17 00:00:00 2001 From: Irene Schena Date: Fri, 1 Feb 2002 17:08:31 +0000 Subject: [PATCH] ---------------------------------------------------------------------- Modified Files: 1) arith.xsl mmlctop.xsl-0.14 mmlextension.xsl xslt_index.txt: added mml presentation for (dis)equalities and new proof elements and some additions for Algebra elements Added Files: 2) mmlnotation.xsl: mml presentation notations ---------------------------------------------------------------------- --- helm/style/arith.xsl | 2 +- helm/style/mmlextension.xsl | 499 ++++++++++++++---------------------- helm/style/mmlnotation.xsl | 343 +++++++++++++++++++++++++ helm/style/xslt_index.txt | 1 + 4 files changed, 539 insertions(+), 306 deletions(-) create mode 100644 helm/style/mmlnotation.xsl diff --git a/helm/style/arith.xsl b/helm/style/arith.xsl index 0751b123c..73616e353 100644 --- a/helm/style/arith.xsl +++ b/helm/style/arith.xsl @@ -61,7 +61,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']"> - + diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 6dce30b65..7e9bd1e5f 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -40,10 +40,12 @@ which generates the toplevel element (see for instance xlink) --> xmlns:xlink="http://www.w3.org/1999/xlink"> - + + + @@ -614,7 +616,10 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + @@ -623,7 +628,10 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + @@ -639,10 +647,16 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + _ - + + + + ) @@ -1000,7 +1014,7 @@ which generates the toplevel element (see for instance xlink) --> - We can prove + We can prove _ @@ -1026,7 +1040,71 @@ which generates the toplevel element (see for instance xlink) --> - we proved + we proved + _ + + + + _ + + + (hide details) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + We can prove + _ + + + _ + (explain) + + + + + + + + + + + + + + + + + + + + + we proved _ @@ -1060,14 +1138,14 @@ which generates the toplevel element (see for instance xlink) --> - + - + @@ -1078,7 +1156,7 @@ which generates the toplevel element (see for instance xlink) --> - We prove + We prove _ @@ -1087,7 +1165,7 @@ which generates the toplevel element (see for instance xlink) --> - by induction on + by induction on _ @@ -1119,7 +1197,7 @@ which generates the toplevel element (see for instance xlink) --> - Case + Case _ @@ -1134,7 +1212,7 @@ which generates the toplevel element (see for instance xlink) --> - By induction hypothesis, we have: + By induction hypothesis, we have: @@ -1540,6 +1618,92 @@ which generates the toplevel element (see for instance xlink) --> + + + + + + + We have the following equality chain: + + + + + + + + + + + + _ + = + + + = + _ + + + + + + + + + + + __ + + + + + + + + + + + + + + + We have the following disequality chain: + + + + + + + + + + + + _ + + + + + _ + + + + + + + + + + + __ + + + + + + + + @@ -1549,7 +1713,7 @@ which generates the toplevel element (see for instance xlink) --> [ - + @@ -1559,7 +1723,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1574,7 +1738,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1591,11 +1755,11 @@ which generates the toplevel element (see for instance xlink) --> - + - β + β @@ -1603,12 +1767,12 @@ which generates the toplevel element (see for instance xlink) --> - + - β - * + β + * @@ -1616,11 +1780,11 @@ which generates the toplevel element (see for instance xlink) --> - + - β + β @@ -1628,12 +1792,12 @@ which generates the toplevel element (see for instance xlink) --> - + - β - * + β + * @@ -1649,7 +1813,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1698,7 +1862,7 @@ which generates the toplevel element (see for instance xlink) --> - we get + we get _ @@ -1716,7 +1880,7 @@ which generates the toplevel element (see for instance xlink) --> - we get + we get _ @@ -1771,282 +1935,6 @@ which generates the toplevel element (see for instance xlink) --> - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - __ - - - - - - = - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - __ - - - - - - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - { - - - - - - - - { - | - - - - - - - - - - - - - } - - - - - - - - - - - - - - - - { - - - , - - - - - - - - - { - - - , - - - - - - - - - - - - - - } - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -2129,3 +2017,4 @@ which generates the toplevel element (see for instance xlink) --> + diff --git a/helm/style/mmlnotation.xsl b/helm/style/mmlnotation.xsl new file mode 100644 index 000000000..a89a2e4b9 --- /dev/null +++ b/helm/style/mmlnotation.xsl @@ -0,0 +1,343 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + + + __ + + + + + + = + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + + + __ + + + + + + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + { + + + + + + + + { + | + + + + + + + + + + + + + } + + + + + + + + + + + + + + + + { + + + , + + + + + + + + + { + + + , + + + + + + + + + + + + + + } + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/helm/style/xslt_index.txt b/helm/style/xslt_index.txt index 0ae6f66a7..8028625ce 100644 --- a/helm/style/xslt_index.txt +++ b/helm/style/xslt_index.txt @@ -24,6 +24,7 @@ mk_meta_graph.xsl mk_meta_theory.xsl mmlctop.xsl-0.14 mmlextension.xsl +mmlnotation.xsl mmltheoryextension.xsl objcontent.xsl objtheorycontent.xsl -- 2.39.2