src/HOL/HOL.thy
changeset 2250 891eb76b8045
parent 1674 33aff4d854e4
child 2260 b59781f2b809