src/HOL/HOL.thy
changeset 80987 e7a926b5b5be
parent 80948 572970d15ab0
child 81092 c92efbf32bfe