src/HOL/HOL.ML
changeset 17171 79ab8ea7b097
parent 15524 2ef571f80a55
child 17274 746bb4c56800