X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=4a801a65402c244e03bbe273c6a4d7a7ba1709a3;hb=57d3a252086d34e56cbdff0693bd07f60dc5d887;hp=21225aa8638e98d0211d15eccc6a4d0ee7498f47;hpb=724c03286dd6d22091490ffdd8f66120c6c09dc8;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 21225aa86..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 + + + + ? + : + _ + + + + + + + + + : + + + := + + + + + + + + + + + + _ + + + + + + + + + + + + + + + @@ -411,10 +512,20 @@ which generates the toplevel element (see for instance xlink) --> - - + + + + + + + + + + + + @@ -613,7 +724,10 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + @@ -622,7 +736,10 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + @@ -638,10 +755,16 @@ which generates the toplevel element (see for instance xlink) --> ( - + + + + _ - + + + + ) @@ -737,7 +860,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -787,7 +910,7 @@ which generates the toplevel element (see for instance xlink) --> _ OF - + | @@ -987,52 +1110,173 @@ which generates the toplevel element (see for instance xlink) --> - - - - + + + + + + + + + + We can prove + _ + + + + + _ + (explain) + + + + + + + + + - We can prove + + + + + + + + _ + + + (hide details) + + + + + + + we proved _ + + + + + + + + + + that is equivalent to _ - (explain) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + We can prove + _ + + + + + _ + (explain) + + + + + + + + + + + + + + - - - - - - - - - - - - - - - we proved - _ - + _ - (hide details) + + (hide details) + - - - - - + + + + + we proved + _ + + + + + + + + + + + + that is equivalent to + _ + + + + + + + + + + + + + + + + + + + @@ -1040,14 +1284,14 @@ which generates the toplevel element (see for instance xlink) --> - + - + @@ -1058,7 +1302,7 @@ which generates the toplevel element (see for instance xlink) --> - We prove + We prove _ @@ -1067,7 +1311,7 @@ which generates the toplevel element (see for instance xlink) --> - by induction on + by induction on _ @@ -1099,7 +1343,7 @@ which generates the toplevel element (see for instance xlink) --> - Case + Case _ @@ -1114,7 +1358,7 @@ which generates the toplevel element (see for instance xlink) --> - By induction hypothesis, we have: + By induction hypothesis, we have: @@ -1520,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 @@ -1553,7 +2008,7 @@ which generates the toplevel element (see for instance xlink) --> - we get + we get _ @@ -1571,7 +2026,7 @@ which generates the toplevel element (see for instance xlink) --> - we get + we get _ @@ -1587,7 +2042,12 @@ which generates the toplevel element (see for instance xlink) --> - + + + + + + @@ -1621,252 +2081,6 @@ which generates the toplevel element (see for instance xlink) --> - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - __ - = - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - __ - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - { - - - - - - - - { - | - - - - - - - - } - - - - - - - - - - - { - - - , - - - - - - - - - { - - - , - - - - - - - - - } - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -1924,7 +2138,16 @@ which generates the toplevel element (see for instance xlink) --> - + + + + + + + + + + @@ -1949,3 +2172,4 @@ which generates the toplevel element (see for instance xlink) --> +