src/HOL/HOL.ML
changeset 3362 0b268cff9344
parent 3003 c5293a17afa6
child 3436 d68dbb8f22d3