src/HOL/Auth/Public.thy
changeset 14722 8e739a6eaf11
parent 14261 6c418d139f74
child 15032 02aed07e01bf