src/HOL/HOL.ML
changeset 21051 c49467a9c1e1
parent 21009 0eae3fb48936
child 21150 405ebd7ba881