src/HOL/HOL.ML
changeset 17184 3d80209e9a53
parent 15524 2ef571f80a55
child 17274 746bb4c56800