src/HOL/HOL.thy
changeset 31409 d8537ba165b5
parent 31299 0c5baf034d0e
child 31804 627d142fce19