|MRG home page - Research - Publications - Software - People|
PG Tips is an additional feature that has been incorporated into Proof General to further assist user-interaction with interactive proof assistants. It is a recommender system that helps ease the proof process by suggesting possible proof steps based on the analysis of previous proofs. Currently, PG Tips is only available for use with Isabelle proofs.
NOTE: Place use "recommender.ml"; at the top of the theory file, below the theory definition. The correct format is shown above.
NOTE: It is advised that the display is set to three pane mode when using PG Tips, as shown above. Use Three Panes can be selected from the menu (Proof-General > Options > Display).
Back to PG Tips Home