src/HOL/Predicate_Compile_Examples/ROOT.ML
changeset 39524 59ebce09ce6e
parent 39225 52960d359969
child 39544 3a07bbc264b2