Conditional Transfer Rule
From MaRDI portal
- A mechanized translation from higher-order logic to set theory
- Automatic Data Refinement
- Comprehending Isabelle/HOL’s Consistency
- Constructive Type Classes in Isabelle
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- From types to sets by local type definition in higher-order logic
- From types to sets by local type definitions in higher-order logic
- Interaction with formal mathematical documents in Isabelle/PIDE
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Local Theory Specifications in Isabelle/Isar
- Natural deduction as higher-order resolution
This page was built for software: Conditional Transfer Rule
