src/HOL/Auth/NS_Public.thy
changeset 49456 fa8302c8dea1
parent 37936 1e4c5015a72e
child 56681 e8d5d60d655e