src/HOL/HOL.ML
changeset 6349 f7750d816c21
parent 6214 0513cfd1a598
child 6433 228237ec56e5