src/HOL/HOL.ML
changeset 6381 ed0c7b4a325d
parent 6214 0513cfd1a598
child 6433 228237ec56e5