src/HOL/HOL.ML
changeset 14387 e96d5c42c4b0
parent 14223 0ee05eef881b
child 15524 2ef571f80a55