src/HOL/HOL.ML
changeset 21088 13348ab97f5a
parent 21009 0eae3fb48936
child 21150 405ebd7ba881