src/HOL/HOL.ML
changeset 16478 d0a1f6231e2f
parent 15524 2ef571f80a55
child 17274 746bb4c56800