src/HOL/IMP/Sec_TypingT.thy
changeset 43397 dba359c0ae3b
parent 43158 686fa0a0696e
child 45015 fdac1e9880eb