src/HOL/HOL.thy
changeset 55775 1557a391a858
parent 55757 9fc71814b8c1
child 56375 32e0da92c786