Sorry, missed all this, because I was away (and the rest of NICTA had a quite busy week).
On 21.11.2013, at 10:56 pm, Makarius <makar...@sketis.net> wrote: > On Wed, 20 Nov 2013, Makarius wrote: > >> Did anybody test WWW_Find? > > WWW_Find is a NICTA-only tool. Did any of the NICTA guys test it in the > Isabelle2013-1 RC phase? Good question. I did not, I assumed others in the group did. Will double-check this week on Isabelle2013-2 RC. > There was also zero feedback about the context selector in the Find panel of > Isabelle/jEdit, e.g. if it can supersede WWW_Find or if it is useless. Neither. It is somewhat useful, but the main use case for WWW_Find is with images that are potentially too big to build yourself or that you don’t have on your machine for some other reason (e.g. too big for a laptop or small desktop). > That context is not fully native in the document model so far, and it would > require a bit more work to make it fit tightly. That work is well-invested > if the resources for WWW_Find maintenance could be freed eventually (by > removing it from the source tree). If the find_theorems panel could connect to a remote resource similar to sledgehammer's remote provers, we could remove WWW_Find. Cheers, Gerwin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
