src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
changeset 80894 3e0ca6af6738
parent 80636 4041e7c8059d