-*- outline -*-

* Summary of Changes for Proof General 3.2 from 3.1


** New instantiations of Proof General!

*** Plastic (http://www.dur.ac.uk/CARG/plastic.html)  (ongoing work)
  
   by Paul Callaghan <P.C.Callaghan@durham.ac.uk>.
   The Plastic system itself is not yet publicly available,
   so this is only included in the developers tar file.


** Generic Changes

*** Improved behaviour of electric terminator

*** Efficiency improvement in parsing
 
  Also works around crash bug in xemacs-21.1.7/SuSE.
  Fix by Markus Wenzel.

*** Added possibility for switching prover's output on/off.

  Already implemented in Coq and Isabelle(/Isar).


** Coq Changes

*** More decoration of Coq output, uses CoqResp mode now

** LEGO Changes

*** Slight change in output during proof: show final discharge messages

** Isabelle Changes

*** Fix for stack overflow in regexp which occurred with large proof states

** Isar Changes

** HOL Changes

*** Output decoration improvements.

** Changes for developers to note

*** No need for match string 1 in proof-shell-proof-completed

*** Changed buffer mode name: pbp-mode -> proof-goals-mode, for uniformity.