src/HOL/HOL.ML
changeset 7699 09d8fd81cc1f
parent 7529 fa534e4f7e49
child 9396 a1b31d61f8e1