src/HOL/HOL.ML
changeset 16877 e92cba1d4842
parent 15524 2ef571f80a55
child 17274 746bb4c56800