src/HOL/Auth/Auth_Public.thy
changeset 73576 b50f8cc8c08e
parent 65538 a39ef48fbee0
equal deleted inserted replaced
73575:23d2adc5489e 73576:b50f8cc8c08e