src/HOL/Auth/Public.thy
changeset 17421 0382f6877b98
parent 16417 9bc16273c2d4
child 17990 86d462f305e0