### 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

BSD License

### Topics

- Tools

### Session Conditional_Transfer_Rule

- CTR_Tools
- IML_UT
- UD
- CTR
- UD_Tests
- CTR_Tests
- Reference_Prerequisites
- CTR_Introduction
- UD_Reference
- CTR_Reference

### Depends on

- SpecCheck - Specification-Based Testing for Isabelle/ML

### Used by

- Extension of Types-To-Sets

### Auto-related entries

- Unification Utilities for 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

## Cite

×

Conditional_Transfer_Rule-AFP

    @article{Conditional_Transfer_Rule-AFP,
      author  = {Mihails Milehins},
      title   = {Conditional Transfer Rule},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Conditional_Transfer_Rule.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Oct 13, 2021 : Isabelle2021
- Sep 14, 2021 : Isabelle2021