src/HOL/HOL.thy
changeset 3339 cfa72a70f2b5
parent 3320 3a5e4930fb77
child 3370 5c5fdce3a4e4