src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 80894 3e0ca6af6738
parent 80634 a90ab1ea6458
child 82695 d93ead9ac6df