src/HOL/Auth/Shared.thy
changeset 69820 dfc5f8294fbc
parent 69597 ff784d5a5bfb
child 76287 cdc14f94c754