HomeIsabelle/Phabricator

lucas - fixed bug with uninstantiated type contexts in eqsubst and added the…

Description

lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)

Details

Provenance
dixonAuthored on
Parents
rISABELLEb4ea8bf8e2f7: -(n::nat) is now regarded as atomic
Branches
Unknown
Tags
Unknown