src/HOL/Auth/NS_Public.thy
changeset 8148 5ef0b624aadb
parent 5434 9b4bed3f394c
child 11104 f2024fed9f0c