src/HOL/Auth/Shared.ML
changeset 2944 283e31f6a4be
parent 2922 580647a879cf
child 3121 cbb6c0c1c58a