src/HOL/Auth/Public.thy
changeset 13028 81c87faed78b
parent 11287 0103ee3082bf
child 13922 75ae4244a596