src/HOL/HOL.thy
changeset 14024 213dcc39358f
parent 13764 3e180bf68496
child 14201 7ad7ab89c402