src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
changeset 79243 0e15387c0300
parent 74561 8e6c973003c8
child 80636 4041e7c8059d