src/HOL/Auth/Public.thy
changeset 32887 85e7ab9020ba
parent 32630 133e4a6474e3
child 37936 1e4c5015a72e