[isabelle-dev] Find theorems and Sledgehammer Panels

Makarius makarius at sketis.net
Wed Sep 25 23:55:26 CEST 2013

On Tue, 24 Sep 2013, Makarius wrote:

> On Mon, 23 Sep 2013, Makarius wrote:
>> With Isabelle/322a3ff42b33 there is now completion for the history text 
>> field behind it.
>> It is again one of these typical instances of spending 2h to make it work 
>> on Linux and Windows, and requiring days or weeks to find out why 
>> Apple/Oracle don't quite manage on Mac OS X: the focus change after 
>> completion selects all text.  (Problem still pending.)
> Apple makes it more difficult to get into its dungeons where the real sources 
> are guarded by dragons

I need to correct this.  The formerly secret Apple sources are part of the 
regular Oracle JDK source forest, e.g. here:


This might eventually give some insight into the important com.apple.laf 
and com.apple.eawt packages.


More information about the isabelle-dev mailing list