[isabelle-dev] Normalise theorem wrt an environment

Makarius makarius at sketis.net
Wed Sep 29 17:49:56 CEST 2021

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.


More information about the isabelle-dev mailing list