Summary of Changes for Proof General 2.2 from 2.1 ------------------------------------------------- Generic Changes --------------- * New function C-c C-f (proof-find) to invoke some prover-specific mechanism to search for theories. [in progress] * Toolbar has five new buttons (State, Context, Info, Command, Help) which invoke commands previously available on keys/menus. [in progress] * Toolbar enablers have been added. Buttons are automatically enabled or disabled as appropriate. This requires XEmacs 20.4 or better for reliable working. * Terminal string now automatically added to command for C-c C-v * Cleaned up example files so all demonstrate same theorem "conj_comms". Would be nice to add more theorems to compare scripts/proofs in different systems. Please send in example scripts! * Shorter buffer names for convenience. * Removed transparent gif from splash screen because XEmacs can't display it nicely. * Documentation updates. * Code cleanups and improvements. Coq Changes ----------- * Set proof-{qed,save}-commands so the toolbar functions work. Isabelle and Isar Changes ------------------------- * Tweaks for input syntax. * Recognize goals of the old form val prems = goal ... Only in the developer's release: -------------------------------- * Provisional instantiation of Proof General for Plastic (http://www.dur.ac.uk/CARG/plastic.html) by Paul Callaghan .