src/HOL/IMP/Sec_TypingT.thy
changeset 69059 70f9826753f6
parent 68776 403dd13cf6e9
child 69597 ff784d5a5bfb