src/HOL/Auth/NS_Public_Bad.ML
changeset 9523 232b09dba0fe
parent 8054 2ce57ef2a4aa