src/HOL/Examples/ML.thy
changeset 82734 89347c0cc6a3
parent 71934 914baafb3da4