src/HOL/HOL.ML
changeset 15771 08cc20626a0f
parent 15524 2ef571f80a55
child 17274 746bb4c56800
equal deleted inserted replaced
15770:90b6433c6093 15771:08cc20626a0f