src/HOL/Auth/Public.thy
changeset 17856 0551978bfda5
parent 16417 9bc16273c2d4
child 17990 86d462f305e0