src/HOL/Examples/ML.thy
changeset 77759 f513f754c026
parent 71934 914baafb3da4