On 29/09/2021 16:42, Kevin Kappelmann wrote:
> We had two different user stories at our chair:
>
> 1. The resolution-based methods use the higher-order unifier. However,
> one might only be interested in results produced by, for example,
> first-order unification when resolving two rules. Hence, a first-order
> unifier was used to obtain an environment, the rules instantiated, and
> then the instantiated rules resolved.
>
> 2. The second use case indeed is tied to unification - I was working on
> an extension to the unifier.
That counts as "dark matter of the Isabelle Universe".
The Isabelle sources are continuously "garbage collected": anything that is
unused, disappears.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
