src/HOL/HOL.ML
changeset 5592 64697e426048
parent 5447 df03d330aeab
child 5760 7e2cf2820684