Session HOL-Predicate_Compile_Examples
View
theory dependencies
Theories
HOL-Library.Predicate_Compile_Alternative_Defs
Examples
Predicate_Compile_Tests
HOL-Library.Predicate_Compile_Quickcheck
File ‹~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML›
Predicate_Compile_Quickcheck_Examples
Specialisation_Examples
IMP_1
IMP_2
IMP_3
IMP_4