Am 17/08/2013 15:20, schrieb Makarius: > 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.
Which can be done safely outside the kernel. > 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. So every application that needs matching should implement it separately? I have seen more elegant designs ;-) Tobias > 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
