src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 44137 ac5cb4c86448
parent 42816 ba14eafef077
child 45450 dc2236b19a3d