src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 59655 5d1b4ab7d173
parent 59582 0fbed69ff081
child 60696 8304fb4fb823