Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
On Thu, 15 Aug 2013, Lawrence Paulson wrote: I think that the only way to achieve the documented behaviour is to replace all schematic variables in the goal by Frees before attempting resolution. If you would do that for the quais-match mode of unify.ML in general it would probably break down everything else. Doing the above in user space instead, in the actual application at hand (which was not explained on this thread so far) it might turn out trivial. Combinators like Subgoal.FOCUS have replaced a lot of old-style tinkering with goals; within the focused parts things are fixed and don't get instantiated by accident. (Tools built on such high-level elements need to be ready to work with renamings of the original schematic variables. This is the normal situation in structured proof elements.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
On Thu, 15 Aug 2013, Lawrence Paulson wrote: On 13 Aug 2013, at 10:35, Lars Noschinski nosch...@in.tum.de wrote: It might be interesting to note that also Unify.matchers is not able to match such term. This old thread on Unify.matchers might be also interesting: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-August/msg00080.html Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: sledgehammer panel
*** Prover IDE -- Isabelle/Scala/jEdit *** * Dockable window Sledgehammer manages asynchronous / parallel sledgehammer runs over existing document sources, independently of normal editing and checking process. This refers to Isabelle/bca3769b6b45. It should be usable already, although rounds 2 and 3 of refinements still need to be done before the coming release, to ensure that the multithreading and interrupting really works. All this has required a few years longer than anticipated. In 2005 Larry had proposed to make everything in Isabelle work concurrently, now we are more or less there. It is now subsumed by the PIDE document model, and the implementation is not so big after all, probably smaller than the earlier isolated attempts taken together (e.g. the first multi-threaded ATP manager from summer 2008.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] The coming release
Dear all, in the past few weeks the coming release has been mentioned in passing several times. So far the precise schedule is not clear, but just from the distance to Isabelle2013 and the amount of material that is about to be finished for Isabelle2013-1, it has to be rather soon after the summer. Since Isabelle is a huge and complex system, things that are relevant for a release need to be known well in advance. (Even such seemingly trivial reforms like subscripts in identifiers have taken much longer than anticipated and are not finished yet.) So the time to point out further issues or pending projects is now -- apart from the well-known HOL-BNF and PIDE improvements that are already underway. In general there is no reason to rush anything on any particular release train, since they are rather frequent anyway. A release is a limit point of consolidation -- the really new things happen after it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] match_tac, schematic and bound variables
Probably you are right. Larry On 17 Aug 2013, at 14:20, Makarius makar...@sketis.net wrote: On Thu, 15 Aug 2013, Lawrence Paulson wrote: I think that the only way to achieve the documented behaviour is to replace all schematic variables in the goal by Frees before attempting resolution. If you would do that for the quais-match mode of unify.ML in general it would probably break down everything else. Doing the above in user space instead, in the actual application at hand (which was not explained on this thread so far) it might turn out trivial. Combinators like Subgoal.FOCUS have replaced a lot of old-style tinkering with goals; within the focused parts things are fixed and don't get instantiated by accident. (Tools built on such high-level elements need to be ready to work with renamings of the original schematic variables. This is the normal situation in structured proof elements.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
