src/HOL/HOL.ML
changeset 5548 5cd3396802f5
parent 5447 df03d330aeab
child 5760 7e2cf2820684