[isabelle-dev] Normalise theorem wrt an environment

[Makarius]

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