src/HOL/HOL.ML
changeset 1627 64ee96ebf32a
parent 1515 4ed79ebab64d
child 1657 a7a6c3fb3cdd