src/HOL/Auth/NS_Public.ML
changeset 9450 c97dba47e504
parent 8054 2ce57ef2a4aa