src/HOL/HOL.ML
changeset 7025 afbd8241797b
parent 6968 7f2977e96a5c
child 7030 53934985426a