src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 55837 154855d9a564
parent 55642 63beb38e9258
child 56490 16d00478b518