Cited in
(19)- From types to sets by local type definition in higher-order logic
- From types to sets by local type definitions in higher-order logic
- On definitions of constants and types in HOL
- A formal proof of the Kepler conjecture
- A verified proof checker for higher-order logic
- ProofPower
- HOL-Omega
- Milawa
- Jitawa
- HOL90
- Light-weight Containers
- Metamath Zero
- HOL Zero's solutions for Pollack-inconsistency
- A formalization and proof checker for Isabelle's metalogic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22--25, 2016. Proceedings
- Flyspecking Flyspeck
- A consistent foundation for Isabelle/HOL
This page was built for software: HOL Zero
