src/HOL/Auth/Public.thy
changeset 4246 c539e702e1d2
parent 3683 aafe719dff14
child 5183 89f162de39cf
equal deleted inserted replaced
4245:b9ce25073cc0 4246:c539e702e1d2