X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=4a801a65402c244e03bbe273c6a4d7a7ba1709a3;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=bb13c876ebcd93bf38997b2c190d2a0b3e258747;hpb=1fff0186531410297e970ba862947b2cbd539fb5;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index bb13c876e..4a801a654 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"> - + + + @@ -179,10 +181,54 @@ which generates the toplevel element (see for instance xlink) --> - + __ - : - + + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ + :? + _ + + + + + ; + + + |- + ? + : + @@ -190,7 +236,7 @@ which generates the toplevel element (see for instance xlink) --> - CORRESPONDING PROOF: + PROOF: @@ -358,6 +404,61 @@ which generates the toplevel element (see for instance xlink) --> + + + + + + + none + + + solid + + + + ? + : + _ + + + + + + + + + : + + + := + + + + + + + + + + + + _ + + + + + + + + + + + + + + + @@ -373,21 +474,27 @@ which generates the toplevel element (see for instance xlink) --> - - : + + + : + + + - - : - + + + : + + @@ -405,10 +512,20 @@ which generates the toplevel element (see for instance xlink) --> - - + + + + + + + + + + + + @@ -417,7 +534,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -433,7 +550,7 @@ which generates the toplevel element (see for instance xlink) --> - + : @@ -607,7 +724,10 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + @@ -616,7 +736,10 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + @@ -632,10 +755,16 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + _ - + + + + ) @@ -731,8 +860,8 @@ which generates the toplevel element (see for instance xlink) --> - - + + @@ -745,10 +874,10 @@ which generates the toplevel element (see for instance xlink) --> _ - + - + @@ -759,7 +888,7 @@ which generates the toplevel element (see for instance xlink) --> |_ - + @@ -781,15 +910,15 @@ which generates the toplevel element (see for instance xlink) --> _ OF - + | - + - + _ END @@ -981,48 +1110,173 @@ which generates the toplevel element (see for instance xlink) --> - - - - - - We can prove - _ - - - - _ - - (explain) - - - - - - - - - - - - - - - - we proved - _ - + + + + + + + + + + We can prove + _ + + + + + _ + (explain) + + + + + + + + + + + + + + + + + + _ - (hide details) + + (hide details) + - - - - - + + + + + we proved + _ + + + + + + + + + + + + that is equivalent to + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + We can prove + _ + + + + + _ + (explain) + + + + + + + + + + + + + + + + + + + + + _ + + + (hide details) + + + + + + + we proved + _ + + + + + + + + + + + + that is equivalent to + _ + + + + + + + + + + + + + + + + + + + @@ -1030,28 +1284,25 @@ which generates the toplevel element (see for instance xlink) --> - + - + - - - - We prove + We prove _ @@ -1060,9 +1311,9 @@ which generates the toplevel element (see for instance xlink) --> - by induction on + by induction on _ - @@ -1070,12 +1321,13 @@ which generates the toplevel element (see for instance xlink) --> - _ - + + + @@ -1091,7 +1343,7 @@ which generates the toplevel element (see for instance xlink) --> - Case + Case _ @@ -1105,7 +1357,9 @@ which generates the toplevel element (see for instance xlink) --> - By induction hypothesis, we have: + + By induction hypothesis, we have: + @@ -1125,7 +1379,9 @@ which generates the toplevel element (see for instance xlink) --> - + + + @@ -1155,6 +1411,7 @@ which generates the toplevel element (see for instance xlink) --> + @@ -1173,8 +1430,6 @@ which generates the toplevel element (see for instance xlink) --> - - @@ -1278,7 +1533,7 @@ which generates the toplevel element (see for instance xlink) --> - Then apply it to + Then apply it to _ @@ -1308,7 +1563,7 @@ which generates the toplevel element (see for instance xlink) --> - In particular, we have + In particular, we have @@ -1343,8 +1598,6 @@ which generates the toplevel element (see for instance xlink) --> - - @@ -1367,7 +1620,7 @@ which generates the toplevel element (see for instance xlink) --> - We proceed by cases to prove + We proceed by cases to prove _ @@ -1376,7 +1629,7 @@ which generates the toplevel element (see for instance xlink) --> - Left: suppose + Left: suppose _ ( @@ -1388,8 +1641,8 @@ which generates the toplevel element (see for instance xlink) --> - _ + _ @@ -1397,7 +1650,7 @@ which generates the toplevel element (see for instance xlink) --> - Right: suppose + Right: suppose _ ( @@ -1416,7 +1669,6 @@ which generates the toplevel element (see for instance xlink) --> - @@ -1439,11 +1691,11 @@ which generates the toplevel element (see for instance xlink) --> - We prove + We prove _ _ - by cases: + by cases: @@ -1493,7 +1745,7 @@ which generates the toplevel element (see for instance xlink) --> : _ - such that + such that _ ( @@ -1512,6 +1764,217 @@ which generates the toplevel element (see for instance xlink) --> + + + + + + + We have the following equality chain: + + + + + + + + + + + + _ + = + + + = + _ + + + + + + + + + + + __ + + + + + + + + + + + + + + + We have the following disequality chain: + + + + + + + + + + + + _ + + + + + _ + + + + + + + + + + + __ + + + + + + + + + + + + + + + + [ + + + + + + + ] + + + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + ( + + ) + + + + + + + + + + + β + + + + + + + + + + + + β + * + + + + + + + + + + + + β + + + + + + + + + + + + β + * + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ERROR @@ -1545,7 +2008,7 @@ which generates the toplevel element (see for instance xlink) --> - we get + we get _ @@ -1563,7 +2026,7 @@ which generates the toplevel element (see for instance xlink) --> - we get + we get _ @@ -1579,7 +2042,12 @@ which generates the toplevel element (see for instance xlink) --> - + + + + + + @@ -1613,256 +2081,6 @@ which generates the toplevel element (see for instance xlink) --> - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - __ - = - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - __ - - - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - { - - - - - - - - { - | - - - - - - - - } - - - - - - - - - - - { - - - , - - - - - - - - - { - - - , - - - - - - - - - } - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -1920,7 +2138,16 @@ which generates the toplevel element (see for instance xlink) --> - + + + + + + + + + + @@ -1946,5 +2173,3 @@ which generates the toplevel element (see for instance xlink) --> - -