src/HOL/HOL.ML
changeset 5648 fe887910e32e
parent 5447 df03d330aeab
child 5760 7e2cf2820684
equal deleted inserted replaced
5647:4e8837255b87 5648:fe887910e32e