src/HOL/Auth/Public.thy
changeset 33155 78c10ce27f09
parent 32630 133e4a6474e3
child 37936 1e4c5015a72e