src/HOL/HOL.ML
changeset 22720 296813d7d306
parent 22218 30a8890d2967