[isabelle-dev] I will start to fix my broken entries in afp-devel now

2012-02-14 Thread Peter Lammich
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

[isabelle-dev] More SPASS with Isabelle

2012-02-14 Thread Jasmin Blanchette
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

Re: [isabelle-dev] Isabelle/jEdit and Toplevel.debug

2012-02-14 Thread Makarius
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