src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 62528 c8c532b22947
parent 62391 1658fc9b2618
child 64542 c7d76708379f