src/HOL/HOL.ML
changeset 1950 97f1c6bf3ace
parent 1918 d898eb4beb96
child 1980 a22ff848be9b