src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 42557 ae0deb39a254
parent 42361 23f352990944
child 42816 ba14eafef077