src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 52778 19fa3e3964f0
parent 52732 b4da1f2ec73f
child 54742 7a86358a3c0b