src/HOL/MicroJava/BV/Typing_Framework_err.thy
changeset 15608 f161fa6f8fd5
parent 15425 6356d2523f73
child 16417 9bc16273c2d4