src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 60107 aedbc0413d30
parent 59582 0fbed69ff081
child 60696 8304fb4fb823