src/HOL/HOL.ML
changeset 5807 bd2d9dd34dfd
parent 5760 7e2cf2820684
child 5809 bacf85370ce0