src/HOL/Auth/Public.thy
changeset 13025 433c57d09d53
parent 11287 0103ee3082bf
child 13922 75ae4244a596