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.
BSD LicenseDepends On
Used by
Topics
Theories
- CTR_Tools
- files/More_Library.ML
- files/More_Binding.ML
- files/More_Type.ML
- files/More_Sort.ML
- files/More_Term.ML
- files/More_Variable.ML
- files/More_Logic.ML
- files/More_Thm.ML
- files/More_Simplifier.ML
- files/More_HOLogic.ML
- files/More_Transfer.ML
- files/CTR_Utilities.ML
- IML_UT
- files/UT_Test_Suite.ML
- UD
- files/UD_With.ML
- files/UD_Consts.ML
- files/UD.ML
- CTR
- files/CTR_Relators.ML
- files/CTR_Foundations.ML
- files/CTR_Algorithm.ML
- files/CTR_Conversions.ML
- files/CTR_Relativization.ML
- files/CTR_Parametricity.ML
- files/CTR_Postprocessing.ML
- files/CTR.ML
- UD_Tests
- files/UD_TEST_UNOVERLOAD_DEFINITION.ML
- CTR_Tests
- files/CTR_TEST_PROCESS_RELATIVIZATION.ML
- files/CTR_TEST_PROCESS_CTR_RELATOR.ML
- Reference_Prerequisites
- files/ISABELLE_HOME/src/Doc/antiquote_setup.ML
- CTR_Introduction
- UD_Reference
- CTR_Reference