Session Conditional_Transfer_Rule
View
theory dependencies
View
document
View
outline
Theories
CTR_Tools
File ‹More_Library.ML›
File ‹More_Binding.ML›
File ‹More_Type.ML›
File ‹More_Sort.ML›
File ‹More_Term.ML›
File ‹More_Variable.ML›
File ‹More_Logic.ML›
File ‹More_Thm.ML›
File ‹More_Simplifier.ML›
File ‹More_HOLogic.ML›
File ‹More_Transfer.ML›
File ‹CTR_Utilities.ML›
SpecCheck.SpecCheck_Base
File ‹util.ML›
File ‹speccheck_base.ML›
File ‹property.ML›
File ‹configuration.ML›
File ‹random.ML›
SpecCheck.SpecCheck_Generators
File ‹gen_types.ML›
File ‹gen_base.ML›
File ‹gen_text.ML›
File ‹gen_int.ML›
File ‹gen_real.ML›
File ‹gen_function.ML›
File ‹gen_term.ML›
File ‹gen.ML›
SpecCheck.SpecCheck_Show
File ‹show_types.ML›
File ‹show_base.ML›
File ‹show_term.ML›
File ‹show.ML›
SpecCheck.SpecCheck_Shrink
File ‹shrink_types.ML›
File ‹shrink_base.ML›
File ‹shrink.ML›
SpecCheck.SpecCheck_Output_Style
File ‹output_style_types.ML›
File ‹output_style_perl.ML›
File ‹output_style_custom.ML›
File ‹output_style.ML›
SpecCheck.SpecCheck
File ‹lecker.ML›
File ‹speccheck.ML›
IML_UT
UD
File ‹UD_With.ML›
File ‹UD_Consts.ML›
File ‹UD.ML›
HOL-Library.Conditional_Parametricity
File ‹conditional_parametricity.ML›
CTR
File ‹CTR_Relators.ML›
File ‹CTR_Foundations.ML›
File ‹CTR_Algorithm.ML›
File ‹CTR_Conversions.ML›
File ‹CTR_Relativization.ML›
File ‹CTR_Parametricity.ML›
File ‹CTR_Postprocessing.ML›
File ‹CTR.ML›
UD_Tests
File ‹UD_TEST_UNOVERLOAD_DEFINITION.ML›
CTR_Tests
File ‹CTR_TEST_PROCESS_RELATIVIZATION.ML›
File ‹CTR_TEST_PROCESS_CTR_RELATOR.ML›
HOL-Library.LaTeXsugar
Reference_Prerequisites
File ‹~~/src/Doc/antiquote_setup.ML›
CTR_Introduction
UD_Reference
CTR_Reference