src/HOL/HOL.thy
changeset 3362 0b268cff9344
parent 3320 3a5e4930fb77
child 3370 5c5fdce3a4e4