X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fmmlextension.xsl;h=b9cd3165ef2bc2e4d1e98ed03d4fb4ce686950a6;hb=d1d5f6ee41209f05c072ba20e3cd50bc774ebff4;hp=049398f9a9539c1d1492d252ad507cd49897e2c2;hpb=3d585511751044f308125da7a71d70e29cc6ca60;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 049398f9a..b9cd3165e 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"> - + + + @@ -412,8 +414,9 @@ which generates the toplevel element (see for instance xlink) --> - + + @@ -613,7 +616,10 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + @@ -622,7 +628,10 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + @@ -638,10 +647,16 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + _ - + + + + ) @@ -987,58 +1002,135 @@ which generates the toplevel element (see for instance xlink) --> - - - + + + + + + + + We can prove + _ + + + _ + (explain) + + + + + + + + + - We can prove + + + + + + + + we proved _ - _ - (explain) + + _ + + + (hide details) + - - - - - - - - - - - - - - we proved - _ - + + + + + + + + + + + + + + + + + + + + + + + + We can prove + _ + + + _ + (explain) + + + + + + + + + + + + - - _ - - - (hide details) - + - - - - - + + + + + + we proved + _ + + + + _ + + + (hide details) + + + + + + + + + + + + + + + + + + @@ -1046,14 +1138,14 @@ which generates the toplevel element (see for instance xlink) --> - + - + @@ -1064,7 +1156,7 @@ which generates the toplevel element (see for instance xlink) --> - We prove + We prove _ @@ -1073,7 +1165,7 @@ which generates the toplevel element (see for instance xlink) --> - by induction on + by induction on _ @@ -1105,7 +1197,7 @@ which generates the toplevel element (see for instance xlink) --> - Case + Case _ @@ -1120,7 +1212,7 @@ which generates the toplevel element (see for instance xlink) --> - By induction hypothesis, we have: + By induction hypothesis, we have: @@ -1526,6 +1618,92 @@ which generates the toplevel element (see for instance xlink) --> + + + + + + + We have the following equality chain: + + + + + + + + + + + + _ + = + + + = + _ + + + + + + + + + + + __ + + + + + + + + + + + + + + + We have the following disequality chain: + + + + + + + + + + + + _ + + + + + _ + + + + + + + + + + + __ + + + + + + + + @@ -1535,9 +1713,9 @@ which generates the toplevel element (see for instance xlink) --> [ - - - + + + ] @@ -1545,9 +1723,9 @@ which generates the toplevel element (see for instance xlink) --> - - - + + + @@ -1560,9 +1738,9 @@ which generates the toplevel element (see for instance xlink) --> - - - + + + @@ -1577,11 +1755,11 @@ which generates the toplevel element (see for instance xlink) --> - - - + + + - β + β @@ -1589,12 +1767,12 @@ which generates the toplevel element (see for instance xlink) --> - - - + + + - β - * + β + * @@ -1602,11 +1780,11 @@ which generates the toplevel element (see for instance xlink) --> - - - + + + - β + β @@ -1614,20 +1792,20 @@ which generates the toplevel element (see for instance xlink) --> - - - + + + - β - * + β + * - - + + @@ -1635,17 +1813,17 @@ which generates the toplevel element (see for instance xlink) --> - - - + + + - - + + @@ -1684,7 +1862,7 @@ which generates the toplevel element (see for instance xlink) --> - we get + we get _ @@ -1702,7 +1880,7 @@ which generates the toplevel element (see for instance xlink) --> - we get + we get _ @@ -1720,7 +1898,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1757,282 +1935,6 @@ which generates the toplevel element (see for instance xlink) --> - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - __ - - - - - - = - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - __ - - - - - - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - { - - - - - - - - { - | - - - - - - - - - - - - - } - - - - - - - - - - - - - - - - { - - - , - - - - - - - - - { - - - , - - - - - - - - - - - - - - } - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -2115,3 +2017,4 @@ which generates the toplevel element (see for instance xlink) --> +