src/HOL/Auth/NS_Shared.ML
changeset 3362 0b268cff9344
parent 3121 cbb6c0c1c58a
child 3441 6d2887123fa0