src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 43258 956895f99904
parent 42816 ba14eafef077
child 45450 dc2236b19a3d