src/HOL/HOL.ML
changeset 5204 858da18069d7
parent 5185 d1067e2c3f9f
child 5228 66925577cefe