new examples of BNF lifting across quotients using a new theory of confluence,
which simplifies the relator subdistributivity proof obligation
(a few new useful notions were added to HOL;
notably the symmetric and equivalence closures of a relation)
Description
Description
Details
Details
- Provenance
traytel Authored on - Parents
- rISABELLEa3f7f00b4fd8: Removed unnecessary and problematic trivial lemma from HOL-Algebra
- Branches
- Unknown
- Tags