Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle-ATP linkup available

Email Gateway (Aug 18 2022 at 10:36):

From: Lawrence Paulson <lp15@cam.ac.uk>
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

Last updated: May 03 2024 at 08:18 UTC