src/HOL/MicroJava/J/Exceptions.thy
changeset 40592 f432973ce0f6
parent 35416 d8d7d1b785af
child 61361 8b5f00202e1a