src/HOL/Examples/ML.thy
changeset 79298 77e4e69fd0e1
parent 71934 914baafb3da4