<div dir="ltr"><p class="MsoNormal" style="margin-bottom:0cm;margin-bottom:.0001pt;background:white"></p><p class="MsoNormal" style="margin-bottom:0.0001pt;background-repeat:initial initial"><span lang="EN-US" style="font-size:9pt;font-family:Arial,sans-serif">Hi,</span></p> <p class="MsoNormal" style="margin-bottom:0.0001pt;background-repeat:initial initial"><span lang="EN-US" style="font-size:9pt;font-family:Arial,sans-serif"> </span></p> <p class="MsoNormal" style="margin-bottom:0.0001pt;background-repeat:initial initial"><span lang="EN-US" style="font-size:9pt;font-family:Arial,sans-serif">I'm a HOL user and I'm looking for porting the multivariate "Integration" theory from HOL Light to HOL.</span></p> <p class="MsoNormal" style="margin-bottom:0.0001pt;background-repeat:initial initial"><span lang="EN-US" style="font-size:9pt;font-family:Arial,sans-serif">For that, I went through the OpenTheory webpage many times, but I'm not sure to understand how the tool can </span></p><p class="MsoNormal" style="margin-bottom:0.0001pt;background-repeat:initial initial"><span lang="EN-US" style="font-size:9pt;font-family:Arial,sans-serif">be helpful in this regard. </span><span style="font-family:Arial,sans-serif;font-size:9pt">May be, I misunderstood the practical side of the tool.</span></p><p class="MsoNormal" style="margin-bottom:0.0001pt;background-repeat:initial initial"><span style="font-family:Arial,sans-serif;font-size:9pt">Could anyone help me for that?</span></p><p class="MsoNormal" style="margin-bottom:0.0001pt;background-repeat:initial initial"><span style="font-family:Arial,sans-serif;font-size:9pt"><br></span></p> <p class="MsoNormal" style="margin-bottom:0.0001pt;background-repeat:initial initial"><span lang="EN-US" style="font-size:9pt;font-family:Arial,sans-serif">Thank you very much</span></p> <p class="MsoNormal" style="margin-bottom:0.0001pt;background-repeat:initial initial"><span lang="EN-US" style="font-size:9pt;font-family:Arial,sans-serif">Maissa</span></p><p></p></div>