src/HOL/Auth/Public.thy
changeset 11295 66925f23ac7f
parent 11287 0103ee3082bf
child 13922 75ae4244a596