src/HOL/HOL.ML
changeset 17836 5d9c9e284d16
parent 17274 746bb4c56800
child 18916 fda5b8dbbef6