src/HOL/IMP/Sec_TypingT.thy
changeset 80150 96f60533ec1d
parent 69597 ff784d5a5bfb