src/HOL/MicroJava/BV/Typing_Framework_err.thy
changeset 13717 78f91fcdf560
parent 13224 6f0928a942d1
child 15425 6356d2523f73
equal deleted inserted replaced
13716:73de0ef7cb25 13717:78f91fcdf560