src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 52303 16d7708aba40
parent 52230 1105b3b5aa77
child 52732 b4da1f2ec73f