Re: [isabelle] "Find Theorems" error

Quoting John Matthews <matthews at>:

I am trying to use the "Find Theorems" command with the latest Isabelle snapshot (Isabelle_04-Jun-2007). However, all that happens is that ProofGeneral brings up a new window called "*Find Theorems*", and then the error message "No such face: :height" in the mini-buffer at the bottom of the window.

This has been fixed in the Proof General CVS now. The window was developed on GNU Emacs so an XEmacs incompatibility slipped through. I will make a new pre-release soon.

I am using pre-release version ProofGeneral-3.7pre070511, on XEmacs version 21.4.15. So far the rest of ProofGeneral has been working fine.

Thanks for the report. If you find more problems which are definitely Proof General problems, please use the trac system at

(Your problem was already there at

- David.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.