src/HOL/ex/predicate_compile.ML
changeset 31460 d97fa41cc600
parent 31440 ee1d5bec4ce3
child 31514 fed8a95f54db
equal deleted inserted replaced
31459:ae39b7b2a68a 31460:d97fa41cc600