src/HOL/HOL.ML
changeset 6953 b3f6c39aaa2e
parent 6513 e0a9459e99fc
child 6968 7f2977e96a5c