src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
changeset 38957 2eb265efa1b0
parent 38956 2e5bf3bc7361
child 39789 533dd8cda12c
equal deleted inserted replaced
38956:2e5bf3bc7361 38957:2eb265efa1b0