src/HOL/HOL.thy
changeset 2330 3eea6b72bb4f
parent 2260 b59781f2b809
child 2368 d394336997cf