src/HOL/Auth/Shared.ML
changeset 4447 b7ee449eb345
parent 4423 a129b817b58a
child 4477 b3e5857d8d99