src/HOL/Auth/Public.thy
changeset 73576 b50f8cc8c08e
parent 69597 ff784d5a5bfb
child 76287 cdc14f94c754