[isabelle-dev] Find theorems and Sledgehammer Panels

Christian Sternagel c.sternagel at gmail.com
Thu Sep 5 14:44:13 CEST 2013


My two cents,

Last time I tried, there was no auto completion available in the input of the find theorem panel. Which makes the variant of typing find_theorems yourself in the main buffer more convenient for me at the moment.

Also I experienced already several "hangs" with this panel as well as the sledgehammer panel. For the former that means that even after waiting for a long time nothing shows up, whereas for the latter the whole main buffer stays in a grayish highlighted state and does no longer produce output in response to edits (and also doesn't respond to clicking cancel).

However, I cannot reliably reproduce either of that yet.

cheers

chris


More information about the isabelle-dev mailing list