src/HOL/HOL.ML
changeset 21083 a1de02f047d0
parent 21009 0eae3fb48936
child 21150 405ebd7ba881