src/HOL/Auth/Public.thy
changeset 31327 ffa5356cc343
parent 30549 d2d7874648bd
child 32149 ef59550a55d3