This article provides a collection of experimental utilities for unoverloading of definitions and synthesis of conditional transfer rules for the object logic Isabelle/HOL of the formal proof assistant Isabelle written in Isabelle/ML.
- Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories
- Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories
- Category Theory for ZFC in HOL III: Universal Constructions
- Conditional Simplification
- IDE: Introduction, Destruction, Elimination