src/HOL/Auth/NS_Shared.ML
changeset 2919 953a47dc0519
parent 2637 e9b203f854ae
child 3121 cbb6c0c1c58a