So if anyone else currently working on that, please tell me
Best,
Peter
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Hi all,
The automatic prover SPASS, integrated in Sledgehammer, now includes many
enhancements, such as properly oriented term simplification, that should make a
difference for Isabelle problems. Thanks to these, SPASS has become more
effective than E, Vampire, or Z3 [1], and this is just the
On Sat, 11 Feb 2012, Florian Haftmann wrote:
In plain old tty days one would get a traceback for exceptions atfer
ML {* Toplevel.debug := true *}
Is this trace somehow accessible by jEdit also?
It is on the same low-level stdout channel as on the TTY or Proof General,
but this is also the