Re: [isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
On Wed, 2013-01-30 at 15:14 +0100, Jasmin Christian Blanchette wrote: First is quite a bit of work, if you want to bring it into a format that Joe Hurd can understand, assuming he even has the time to look into it. It's probably not worth the effort then. Like you said, this kind of behavior can happen. To suppress the warning, one trick is to ensure that the theorem has no name hint, e.g. mythm[THEN asm_rl] Good to know that there is a workaround. [*] A rule of thumb I remember from industry was to wait until we had the same feature request at least three times before implementing anything. That of course made more sense w.r.t. a large user base (~ 10 000 to 100 000) than for the Isabelle community. Some projects let users vote (+1) on feature requests. Of course, as Steve Jobs put it: A lot of times, people don't know what they want until you show it to them. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
On Wed, 30 Jan 2013, Tjark Weber wrote: Some projects let users vote (+1) on feature requests. Of course, as Steve Jobs put it: A lot of times, people don't know what they want until you show it to them. It is usually better to provide things that people *need*, but that is even harder to find out. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Initialisation of session and nodes: What's changed?
Hi, I have been writing a tool that interfaces with the Isabelle/Scala API, and have previously (with Isabelle 2012) been using the example at https://bitbucket.org/pide/pide_examples/src/5ac145e991f9/ex.scala?at=default to load theories and run the prover, so that I can collect output and process theory semantic information as needed. As the instance method Session.edit_node no longer exists, may I ask what the current method for loading nodes and running the prover is, please? Thanks, Avi ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
