Abstract
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.
License
Topics
Session Conditional_Transfer_Rule
- CTR_Tools
- IML_UT
- UD
- CTR
- UD_Tests
- CTR_Tests
- Reference_Prerequisites
- CTR_Introduction
- UD_Reference
- CTR_Reference
Used by
Auto-related entries
- 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