<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">What I’m requesting requires no sophistication at all. It is merely to automate what we currently do by copying from one window and pasting to another, while inserting “fix”, “assume” and “show” in the obvious places.<br class=""><div class="">
<span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 11px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0; "><div class="">Larry</div></span>

</div>
<br class=""><div><blockquote type="cite" class=""><div class="">On 9 Jul 2017, at 16:32, Lars Hupel <<a href="mailto:hupel@in.tum.de" class="">hupel@in.tum.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="font-family: LucidaGrande; font-size: 13px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">I currently supervise a student who's investigating proof refactoring. One possible outcome of this would be a tool that also does what you suggested. It's a little too early to tell, though.</span></div></blockquote></div><br class=""></body></html>