src/HOL/Auth/Shared.ML
changeset 5760 7e2cf2820684
parent 5535 678999604ee9
child 6308 76f3865a2b1d