Hi, would it be possible to run current Proof General with Isabelle 2005?
Proof General documentation, section 12 Isabelle Proof General writes in the first paragraph: -- Isabelle provides its own way to invoke Proof General via the isabelle command. Running isabelle emacs starts an Emacs session with Isabelle Proof General. -- My Isabelle 2005 installation says $ ./isabelle emacs Unknown logic "emacs" -- no heap file found in: /home/gbuday/isabelle/heaps/polyml-5.6_x86-linux /home/gbuday/prooftheory/Isabelle2005-for-PolyML-5.6/heaps/polyml-5.6_x86-li nux Is "isabelle emacs" a later-than-2005 feature of Isabelle? I tried the other way around, starting emacs and opening an Isabelle theory file. I have the following .emacs: (load "~/.emacs.d/lisp/PG/generic/proof-site") (setq isabelle-program-name-override "/home/gbuday/prooftheory/Isabelle2005-for-PolyML-5.6/bin/isabelle") and I did the PG installation according to https://proofgeneral.github.io/ Quick Installation Proof General did not load. What do you recommend to make it work? Best - Gergely _______________________________________________ ProofGeneral mailing list ProofGeneral@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral