src/HOL/HOL.ML
changeset 21145 87a03f9b7db2
parent 21009 0eae3fb48936
child 21150 405ebd7ba881