Re: [isabelle] Tab completion slow in Isabelle2014-RC2
Am 08.08.14 14:19, schrieb Makarius:
Well I'd like a voice interface where I just explain the proof idea and
sledgehammer and friends pick up keywords to generate a proof from that.
But maybe let's focus on what can be improved on the current state of
On Fri, 8 Aug 2014, Joachim Breitner wrote:
But UI guided interaction will always be limited in expressiveness
and efficiency, compared to a textual interface. There is a reason
why we _write_ Isar, and do not use a “proof block panel” to click
together the fixes and assumes, and elsewhere select the initial
Both the writing and clicking that is sketched here is cumbersome, and
conceptually not really different. A more high-level editing model of
interactice proof documents is required, and apply scripts should be
left behind altogether.
I've started working on more than 15 years ago, but even today people
still think of the source text as a "script" that is somehow linear.
This archive was generated by a fusion of
Pipermail (Mailman edition) and