src/HOL/Auth/NS_Public.thy
changeset 31106 9a1178204dc0
parent 23746 a455e69c31cc
child 32960 69916a850301
equal deleted inserted replaced
31105:95f66b234086 31106:9a1178204dc0