src/HOL/HOL.ML
changeset 4351 36b28f78ed1b
parent 4302 2c99775d953f
child 4467 bd05e2a28602