src/HOL/HOL.ML
changeset 2647 83c9bdff7fdc
parent 2562 d571d6660240
child 3003 c5293a17afa6