[isabelle] Isabelle-ATP linkup available

A complete working version of the Isabelle-ATP linkup is now available in the development snapshot. For best results, it should be used with a recent version of Proof General. Automatic theorem provers (E, SPASS or Vampire) can be applied to the current set of subgoals with a single mouse click. More information is available: <http://www.cl.cam.ac.uk/research/hvg/Isabelle/atp-linkup.html>

Larry Paulson

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